mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- At an invertible map `e : M →L[R] M₂` between Banach spaces, the operation of
inversion is `C^n`, for all `n`.  -/
ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse : ∀ {𝕜 : 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 ℕ∞}
  [CompleteSpace E] {e : E →L[𝕜] F}, e.IsInvertible → ContDiffAt 𝕜 n ContinuousLinearMap.inverse e
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- If `thm` can be used to rewrite `e`, return the rewrite.  -/
Mathlib.Tactic.LibraryRewrite.checkRewrite : Lean.Expr → Lean.Expr → Bool → Lean.MetaM (Option Mathlib.Tactic.LibraryRewrite.Rewrite)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The class `[ValuativeRel R]` class introduces an operator `x ≤ᵥ y : Prop` for `x y : R`
which is the natural relation arising from (the equivalence class of) a valuation on `R` when `R`
is a ring. More precisely, if `v` is a valuation on `R` then the associated relation is
`x ≤ᵥ y ↔ v x ≤ v y`. Use this class to talk about the case where `R` is equipped
with an equivalence class of valuations.  -/
ValuativeRel : (R : Type u_1) → [Semiring R] → Type u_1
-- Mathlib.Data.List.Sort
StrictMono.sortedGE_listMap : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {l : List α},
  StrictMono f → ((List.map f l).SortedGE ↔ l.SortedGE)
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_add : ∀ (m n : ℕ∞), ↑(m + n) = ↑m + ↑n
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.linearMapLeftRight : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_4} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {P : Type u_5} [inst_7 : AddCommMonoid P] [inst_8 : Module R P] {Q : Type u_6} [inst_9 : AddCommMonoid Q]
  [inst_10 : Module R Q] [inst_11 : Module S P] [inst_12 : IsScalarTower R S P] [inst_13 : Module S Q]
  [inst_14 : IsScalarTower R S Q] [Module.Free R M] [Module.Finite R M] {α : M →ₗ[R] P} (j : IsBaseChange S α)
  {β : N →ₗ[R] Q}, IsBaseChange S β → IsBaseChange S (j.linearMapLeftRightHom β)
-- Init.Data.SInt.Lemmas
Int8.toUInt8_ofNat : ∀ {n : ℕ}, Int8.toUInt8 (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_union : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : DecidableEq β] {s₁ s₂ : Finset β} (h₁ : s₁.Nonempty)
  (h₂ : s₂.Nonempty) (f : β → α), (s₁ ∪ s₂).sup' ⋯ f = s₁.sup' h₁ f ⊔ s₂.sup' h₂ f
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallyInjectiveFunYonedaGluedToSheaf : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)),
  CategoryTheory.Sheaf.IsLocallyInjective (AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf hf)
-- Mathlib.Data.Seq.Defs
Stream'.Seq.ofList_injective : ∀ {α : Type u}, Function.Injective Stream'.Seq.ofList
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.SafePrefixState : Type
-- Mathlib.RingTheory.WittVector.MulP
WittVector.bind₁_wittMulN_wittPolynomial : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n k : ℕ),
  (MvPolynomial.bind₁ (WittVector.wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- The map makes the triangle with the two natural transformations commute  -/
CategoryTheory.Limits.IsLimit.fac : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (self : CategoryTheory.Limits.IsLimit t)
  (s : CategoryTheory.Limits.Cone F) (j : J), CategoryTheory.CategoryStruct.comp (self.lift s) (t.π.app j) = s.π.app j
-- Init.Data.Range.Polymorphic.Basic
/-- Checks whether the range contains any value.

This function returns a meaningful value given `LawfulUpwardEnumerable` and
`LawfulUpwardEnumerableLeast?` instances.
 -/
Std.Rii.isEmpty : {α : Type u} → [Std.PRange.Least? α] → Std.Rii α → Bool
-- Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic
/-- Implementation detail for `AlgebraicCycle.map`: function used to define the coefficient of the
pushforward of a cycle `c` at a point `z = f x`.
 -/
AlgebraicGeometry.AlgebraicCycle.mapCoeff : {X : AlgebraicGeometry.Scheme} →
  {N : Type u_2} → [DecidableEq N] → {Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → (↥X → N) → (↥Y → N) → ↥X → ℕ
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- The image of a pre-path object by a functor.  -/
HomotopicalAlgebra.PrepathObject.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      HomotopicalAlgebra.PrepathObject X →
        {D : Type u_1} →
          [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
            (F : CategoryTheory.Functor C D) → HomotopicalAlgebra.PrepathObject (F.obj X)
-- Mathlib.Topology.Algebra.UniformConvergence
instMonoidUniformFun : {α : Type u_1} → {β : Type u_2} → [Monoid β] → Monoid (UniformFun α β)
-- Mathlib.Algebra.Group.WithOne.Basic
AddEquiv.withZeroCongr_trans : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Add α] [inst_1 : Add β] [inst_2 : Add γ] (e₁ : α ≃+ β) (e₂ : β ≃+ γ),
  e₁.withZeroCongr.trans e₂.withZeroCongr = (e₁.trans e₂).withZeroCongr
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L),
  CategoryTheory.CategoryStruct.comp (CochainComplex.cm5b.i f) (CochainComplex.cm5b.p K L) = f
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.lt_total : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (f g : CauSeq α abs),
  f < g ∨ f ≈ g ∨ g < f
-- Mathlib.Tactic.Ring.Common
/-- Two monomials are said to "overlap" if they differ by a constant factor, in which case the
constants just add. When this happens, the constant may be either zero (if the monomials cancel)
or nonzero (if they add up); the zero case is handled specially.
 -/
Mathlib.Tactic.Ring.Common.Overlap : {u : Lean.Level} → {α : Q(Type u)} → (Q(«$α») → Type) → Q(CommSemiring «$α») → Q(«$α») → Type
-- Mathlib.MeasureTheory.Function.UnifTight
/-- Lemma used in `tendsto_Lp_of_tendsto_ae`.  -/
_private.Mathlib.MeasureTheory.Function.UnifTight.0.MeasureTheory.ae_tendsto_ae_congr : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup β] {μ : MeasureTheory.Measure α}
  {f f' : ℕ → α → β} {g g' : α → β},
  (∀ (n : ℕ), f n =ᵐ[μ] f' n) →
    g =ᵐ[μ] g' →
      (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
        ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f' n x) Filter.atTop (nhds (g' x))
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  {m₁ m₂ : Std.DHashMap.Raw α β} {h₁ : 0 < m₁.buckets.size} {h₂ : 0 < m₂.buckets.size},
  Std.DHashMap.Internal.Raw.WFImp m₁ →
    Std.DHashMap.Internal.Raw.WFImp ↑(Std.DHashMap.Internal.Raw₀.inter ⟨m₁, h₁⟩ ⟨m₂, h₂⟩)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Whiskering an exact functor by an exact functor yields an exact functor.  -/
CategoryTheory.ExactFunctor.whiskeringLeft : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            CategoryTheory.Functor (C ⥤ₑ D) (CategoryTheory.Functor (D ⥤ₑ E) (C ⥤ₑ E))
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.ne_empty_of_mem : ∀ {α : Type u} {f : Ultrafilter α} {s : Set α}, s ∈ f → s ≠ ∅
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_const_add : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring 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] [instCFC : ContinuousFunctionalCalculus R A p] (r : R) (f : R → R)
  (a : A),
  autoParam (ContinuousOn f (spectrum R a)) cfc_const_add._auto_1 →
    autoParam (p a) cfc_const_add._auto_3 → cfc (fun x => r + f x) a = (algebraMap R A) r + cfc f a
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_zero_measure : ∀ {E : Type u_2} {mE : MeasurableSpace E} {t : E} [inst : SeminormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E],
  MeasureTheory.charFun 0 t = 0
-- Mathlib.Algebra.Regular.SMul
IsRightRegular.isSMulRegular : ∀ {R : Type u_1} [inst : Mul R] {c : R}, IsRightRegular c → IsSMulRegular R (MulOpposite.op c)
-- Batteries.Data.Array.Basic
/-- Check whether a subarray contains a given element.
 -/
Subarray.contains : {α : Type u_1} → [BEq α] → Subarray α → α → Bool
-- Mathlib.Data.Quot
/-- Map a function `f : α → β → γ` that sends equivalent elements to equivalent elements
to a function `f : Quotient sa → Quotient sb → Quotient sc`. Useful to define binary operations
on quotients. This is a version of `Quotient.map₂` using `Setoid.r` instead of `≈`.  -/
Quotient.map₂' : {α : Sort u_1} →
  {β : Sort u_2} →
    {γ : Sort u_3} →
      {s₁ : Setoid α} →
        {s₂ : Setoid β} →
          {s₃ : Setoid γ} →
            (f : α → β → γ) →
              (∀ ⦃a₁ a₂ : α⦄, s₁ a₁ a₂ → ∀ ⦃b₁ b₂ : β⦄, s₂ b₁ b₂ → s₃ (f a₁ b₁) (f a₂ b₂)) →
                Quotient s₁ → Quotient s₂ → Quotient s₃
-- Mathlib.Data.Fintype.BigOperators
Fintype.prod_sum_type : ∀ {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : CommMonoid M]
  (f : α₁ ⊕ α₂ → M), ∏ x, f x = (∏ a₁, f (Sum.inl a₁)) * ∏ a₂, f (Sum.inr a₂)
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roc.size.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (lower : α) (h_1 : Unit → motive none)
  (h_2 : (lower : α) → motive (some lower)),
  (match some lower with
    | none => h_1 ()
    | some lower => h_2 lower) =
    h_2 lower
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
/-- **Alias** of the reverse direction of `Matrix.one_fromCols_isTotallyUnimodular_iff`. -/
Matrix.IsTotallyUnimodular.one_fromCols : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] [inst_1 : DecidableEq m] (A : Matrix m n R),
  A.IsTotallyUnimodular → (Matrix.fromCols 1 A).IsTotallyUnimodular
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvexHull_subset_closedAbsConvexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] [inst_4 : TopologicalSpace E] {s : Set E}, (absConvexHull 𝕜) s ⊆ (closedAbsConvexHull 𝕜) s
-- Mathlib.Tactic.FunProp.Theorems
/-- There are four types of theorems:
- lam - theorem about basic lambda calculus terms
- function - theorem about a specific function(declared or free variable) in specific arguments
- mor - special theorems talking about bundled morphisms/DFunLike.coe
- transition - theorems inferring one function property from another

Examples:
- lam
  ```
  theorem Continuous_id : Continuous fun x ↦ x
  theorem Continuous_comp (hf : Continuous f) (hg : Continuous g) : Continuous fun x ↦ f (g x)
  ```
- function
  ```
  theorem Continuous_add : Continuous (fun x ↦ x.1 + x.2)
  theorem Continuous_add (hf : Continuous f) (hg : Continuous g) :
      Continuous (fun x ↦ (f x) + (g x))
  ```
- mor - the head of function body has to be `DFunLike.coe`
  ```
  theorem ContDiff.clm_apply {f : E → F →L[𝕜] G} {g : E → F}
      (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
      ContDiff 𝕜 n fun x ↦ (f x) (g x)
  theorem clm_linear {f : E →L[𝕜] F} : IsLinearMap 𝕜 f
  ```
- transition - the conclusion has to be in the form `P f` where `f` is a free variable
  ```
  theorem linear_is_continuous [FiniteDimensional ℝ E] {f : E → F} (hf : IsLinearMap 𝕜 f) :
      Continuous f
  ```
 -/
Mathlib.Meta.FunProp.Theorem : Type
-- Init.Data.Rat.Lemmas
/-- Alternative statement of `ofScientific_def`.
 -/
Rat.ofScientific_def' : ∀ {m : ℕ} {s : Bool} {e : ℕ}, OfScientific.ofScientific m s e = ↑m * 10 ^ if s = true then -↑e else ↑e
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.mkOfLE : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr × Option Lean.Expr)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isoSpec_Spec_hom : ∀ (R : CommRingCat),
  (AlgebraicGeometry.Spec R).isoSpec.hom = AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.ΓSpecIso R).hom
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.eq_1 : ∀ (α : Type u_1) (n : ℕ), Set.powersetCard α n = {s | s.card = n}
-- Mathlib.Logic.ExistsUnique
existsUnique_false : ∀ {α : Sort u_1}, ¬∃! x, False
-- Mathlib.InformationTheory.Hamming
hammingDist_le_card_fintype : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i},
  hammingDist x y ≤ Fintype.card ι
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.lipschitz : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [IsometryClass F α β] (f : F), LipschitzWith 1 ⇑f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.fun_add : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Add β]
  [ContinuousAdd β],
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun i => f i + g i
-- Mathlib.Analysis.Calculus.FDeriv.Linear
ContinuousLinearMap.hasFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E →L[𝕜] F) {x : E} {s : Set E}, HasFDerivWithinAt (⇑f) f s x
-- Init.Data.Array.Lemmas
Array.findSomeRevM?_eq_findSomeM?_reverse : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m (Option β)}
  {xs : Array α}, Array.findSomeRevM? f xs = Array.findSomeM? f xs.reverse
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∪ t₂)[k]? = t₁[k]?
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The identity 2-morphism as a term of `normalExpr`.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.idM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
      [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] →
        Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.NormalExpr
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instAddActionOfVAddAssocClass : {M : Type u_3} →
  {X : Type u_4} →
    [inst : AddMonoid M] →
      {S : AddSubmonoid M} →
        [inst_1 : AddOreLocalization.AddOreSet S] →
          [inst_2 : AddAction M X] →
            {R : Type u_5} →
              [inst_3 : AddMonoid R] →
                [inst_4 : AddAction R M] →
                  [VAddAssocClass R M M] →
                    [inst_6 : AddAction R X] → [VAddAssocClass R M X] → AddAction R (AddOreLocalization S X)
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.subarrayMeasure_cons : ∀ {α : Type u_1} {β : Type u_2} (es : Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)))
  (h : 0 < Std.Slice.size es),
  Lean.PersistentHashMap.subarrayMeasure es = es[0].measure + Lean.PersistentHashMap.subarrayMeasure (es.drop 1)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero_assoc : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤)))
  (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (CommRingCat.of ↥(𝒜 0)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.fromOfGlobalSections 𝒜 f hf)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero 𝒜) h) =
    CategoryTheory.CategoryStruct.comp X.toSpecΓ
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (f.comp (algebraMap (↥(𝒜 0)) A)))) h)
-- Mathlib.Topology.Gluing
TopCat.GlueData.open_image_open : ∀ (D : TopCat.GlueData) (i : D.J) (U : TopologicalSpace.Opens ↑(D.U i)),
  IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) '' ↑U)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.inter_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp]
  {t₃ t₄ : Std.TreeSet.Raw α cmp}, t₁.WF → t₂.WF → t₃.WF → t₄.WF → t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ ∩ t₂).Equiv (t₃ ∩ t₄)
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.integrable_toReal_condExpKernel : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s : Set Ω},
  MeasurableSet s → MeasureTheory.Integrable (fun ω => ((ProbabilityTheory.condExpKernel μ m) ω).real s) μ
-- Mathlib.Algebra.Group.Torsion
/-- Alias of `zpow_left_inj`, for ease of discovery alongside `zsmul_le_zsmul_iff'` and
`zsmul_lt_zsmul_iff'`.  -/
zpow_eq_zpow_iff' : ∀ {G : Type u_2} [inst : Group G] [IsMulTorsionFree G] {n : ℤ} {a b : G}, n ≠ 0 → (a ^ n = b ^ n ↔ a = b)
-- Mathlib.Data.List.Sigma
List.Perm.kunion_left : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (l : List (Sigma β)) {l₁ l₂ : List (Sigma β)},
  l₁.NodupKeys → l₁.Perm l₂ → (l.kunion l₁).Perm (l.kunion l₂)
-- Mathlib.Order.GaloisConnection.Defs
/-- Make a `GaloisCoinsertion` between `αᵒᵈ` and `βᵒᵈ` from a `GaloisInsertion` between
`α` and `β`.  -/
GaloisInsertion.dual : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {u : α → β} →
          {l : β → α} →
            GaloisInsertion l u →
              GaloisCoinsertion (⇑OrderDual.toDual ∘ u ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ l ∘ ⇑OrderDual.ofDual)
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.instIsIsoFunctorαCategoryToNatTransHomHom : ∀ {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G), CategoryTheory.IsIso e.hom.toNatTrans
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- The Möbius function which inverts `zeta` as an element of the incidence algebra.  -/
IncidenceAlgebra.mu : (𝕜 : Type u_2) →
  {α : Type u_5} →
    [inst : AddCommGroup 𝕜] →
      [One 𝕜] → [inst_2 : Preorder α] → [LocallyFiniteOrder α] → [DecidableEq α] → IncidenceAlgebra 𝕜 α
-- Mathlib.Topology.SeparatedMap
IsSeparatedMap.comp_right : ∀ {X : Type u_1} {Y : Sort u_2} {A : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace A] {f : X → Y},
  IsSeparatedMap f → ∀ {g : A → X}, Continuous g → Function.Injective g → IsSeparatedMap (f ∘ g)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
UpperHalfPlane.instSFiniteComapComplexCoeVolume : MeasureTheory.SFinite (MeasureTheory.Measure.comap UpperHalfPlane.coe MeasureTheory.volume)
-- Lean.Meta.ReduceEval
Lean.Meta.instReduceEvalBool : Lean.Meta.ReduceEval Bool
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.grpObjObj.eq_1 : ∀ {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} [inst_4 : F.Monoidal] {G : C} [inst_5 : CategoryTheory.GrpObj G],
  CategoryTheory.Functor.grpObjObj =
    { toMonObj := CategoryTheory.Functor.monObjObj G, inv := F.map CategoryTheory.GrpObj.inv, left_inv := ⋯,
      right_inv := ⋯ }
-- Init.Data.List.Sublist
List.Sublist.refl : ∀ {α : Type u_1} (l : List α), l.Sublist l
-- Init.Data.UInt.Bitwise
UInt16.ofFin_or : ∀ (a b : Fin UInt16.size), UInt16.ofFin (a ||| b) = UInt16.ofFin a ||| UInt16.ofFin b
-- Mathlib.Topology.ContinuousMap.LocallyConstant
LocallyConstant.toContinuousMapMonoidHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Monoid Y]
  [inst_3 : ContinuousMul Y] (f : LocallyConstant X Y), LocallyConstant.toContinuousMapMonoidHom f = ↑f
-- Mathlib.Topology.Algebra.Group.Pointwise
singleton_mul_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Group α] [ContinuousConstSMul α α] {s : Set α} (a : α) {b : α},
  s ∈ nhds b → {a} * s ∈ nhds (a * b)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false},
  t.get? (t.max he) = some (t.max he)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_ι : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (U : ↑X.affineOpens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom h U) (I.glueDataObjι U) =
    J.glueDataObjι U
-- Init.Data.SInt.Basic
/-- Converts an arbitrary-precision integer to a word-sized signed integer, wrapping around on over- or
underflow.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.ofInt : ℤ → ISize
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_add_cancel_left : ∀ {m n k i : ℤ}, (i + m).fmod n = (i + k).fmod n ↔ m.fmod n = k.fmod n
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_minKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false → ∀ {fallback : α}, Std.Internal.List.containsKey (Std.Internal.List.minKeyD l fallback) l = true
-- Mathlib.Algebra.Group.Equiv.TypeTags
MulEquiv.toAdditive_apply_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : MulOneClass G] [inst_1 : MulOneClass H] (f : G ≃* H) (a : Additive G),
  (MulEquiv.toAdditive f) a = (MonoidHom.toAdditive f.toMonoidHom) a
-- Mathlib.RingTheory.IdealFilter.Basic
/-- **Axiom T4.** See [stenstrom1975].  -/
IdealFilter.IsGabriel.gabriel_closed : ∀ {A : Type u_1} {inst : Ring A} {F : IdealFilter A} [self : F.IsGabriel] (I : Ideal A),
  (∃ J ∈ F, ∀ x ∈ J, Submodule.colon I {x} ∈ F) → I ∈ F
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.range_eq_map : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S), f.range = Subring.map f ⊤
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
/-- Reinterpret a C⋆-algebra `A` as a `CStarModule` over itself.  -/
WithCStarModule.instCStarModule : {A : Type u_1} → [inst : NonUnitalCStarAlgebra A] → [inst_1 : PartialOrder A] → [StarOrderedRing A] → CStarModule A A
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_roo_eq_none : ∀ {i : ℕ} {m n : ℤ}, (n - (m + 1)).toNat ≤ i → (m<...n).toList[i]? = none
-- Init.Data.UInt.Lemmas
UInt32.size_le_usizeSize : UInt32.size ≤ USize.size
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app : ∀ (X : CategoryTheory.Limits.WalkingParallelPair),
  CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.counitIso.hom.app X = CategoryTheory.eqToHom ⋯