mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.Inv
derivWithin_fun_inv' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'},
  DifferentiableWithinAt 𝕜 c s x → c x ≠ 0 → derivWithin (fun x => (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The basis on the cotangent space of the constructed presentation.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.basis : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) →
                    [Nontrivial S] →
                      Module.Basis (Unit ⊕ σ) S
                        (Algebra.Generators.PresentationOfFreeCotangent.Aux.pres✝ D).toExtension.Cotangent
-- Mathlib.Data.Holor
HolorIndex.take_take : ∀ {ds₁ ds₂ ds₃ : List ℕ} (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)), t.assocRight.take = t.take.take
-- Std.Internal.Do.WP.Basic
/-- `Option` is a WPMonad with `Prop` assertions and a single `Prop` exception postcondition.  -/
Std.Internal.Do.Option.instWPMonad : Std.Internal.Do.WPMonad Option Prop Prop
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
LinearMap.funLeft.eq_1 : ∀ (R : Type u_1) (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : Type u_9}
  {n : Type u_10} (f : m → n), LinearMap.funLeft R M f = { toFun := fun x => x ∘ f, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.RingTheory.SimpleModule.Basic
Submodule.quotientEquivOfIsCompl.congr_simp : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p q : Submodule R E)
  (h : IsCompl p q), p.quotientEquivOfIsCompl q h = p.quotientEquivOfIsCompl q h
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instSMul : (A : Type u_3) → (E : Type u_4) → {R : Type u_5} → [SMul R E] → SMul R (WithCStarModule A E)
-- Mathlib.Algebra.Group.Units.Equiv
val_toUnits_apply : ∀ {G : Type u_5} [inst : Group G] (x : G), ↑(toUnits x) = x
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H0IsoOfIsTrivial_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial]
  (x : ↑(groupHomology.cycles A 0)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H0IsoOfIsTrivial A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.π A 0)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.cyclesIso₀ A).hom) x
-- Init.Data.List.TakeDrop
List.take_length : ∀ {α : Type u_1} {l : List α}, List.take l.length l = l
-- Lean.Elab.Parallel
/-- Runs a list of CoreM computations in parallel (without cancellation hook).

Returns an iterator that yields results in completion order, wrapped in `Except Exception α`.
 -/
Lean.Core.CoreM.parIterGreedy : {α : Type} → List (Lean.CoreM α) → Lean.CoreM (Std.IterM Lean.CoreM (Except Lean.Exception α))
-- Mathlib.Combinatorics.Graph.Delete
Graph.restrict_mono_left : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, H ≤ G → ∀ (F : Set β), H.restrict F ≤ G.restrict F
-- Std.Data.HashMap.Basic
Std.HashMap.instEmptyCollection : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → EmptyCollection (Std.HashMap α β)
-- Mathlib.Analysis.Analytic.Constructions
/-- Finite products of analytic functions are analytic  -/
Finset.analyticAt_prod : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {α : Type u_9} {A : Type u_10} [inst_3 : NormedCommRing A] [inst_4 : NormedAlgebra 𝕜 A]
  {f : α → E → A} {c : E} (N : Finset α), (∀ n ∈ N, AnalyticAt 𝕜 (f n) c) → AnalyticAt 𝕜 (∏ n ∈ N, f n) c
-- Mathlib.RingTheory.Unramified.LocalRing
/-- [Stacks Tag 00UW](https://stacks.math.columbia.edu/tag/00UW) ((1)) -/
Algebra.FormallyUnramified.map_maximalIdeal : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing R] [inst_4 : IsLocalRing S] [IsLocalHom (algebraMap R S)] [Algebra.EssFiniteType R S]
  [Algebra.FormallyUnramified R S], Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) = IsLocalRing.maximalIdeal S
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_congr' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] [inst_1 : NormedAddCommGroup γ] {f : α → β} {g : α → γ},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      (∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) → (MeasureTheory.Integrable f μ ↔ MeasureTheory.Integrable g μ)
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Suggest replacing a sequence of tactics with `grind` if that also solves the goal.  -/
linter.tacticAnalysis.terminalToGrind : Lean.Option Bool
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.smul_closedEBall`. -/
EMetric.smul_closedBall : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [IsIsometricSMul G X] (c : G) (x : X) (r : ENNReal), c • Metric.closedEBall x r = Metric.closedEBall (c • x) r
-- Mathlib.Data.Complex.Basic
Complex.ofReal_nsmul : ∀ (n : ℕ) (r : ℝ), ↑(n • r) = n • ↑r
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyLT : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.TransOrd α] →
        (k : α) → (t : Std.DTreeMap.Internal.Impl α β) → t.Ordered → (∃ a ∈ t, compare a k = Ordering.lt) → α
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abv_one : ∀ {S : Type u_5} [inst : Ring S] [inst_1 : PartialOrder S] {R : Type u_6} [inst_2 : Semiring R] (abv : R → S)
  [IsAbsoluteValue abv] [IsDomain S] [Nontrivial R], abv 1 = 1
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.nonunits_injective : ∀ {K : Type u} [inst : Field K], Function.Injective ValuationSubring.nonunits
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.support_integralNormalization_subset : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.integralNormalization.support ⊆ p.support
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_eq_some_maxKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {fallback : α}, t.isEmpty = false → t.maxKey? = some (t.maxKeyD fallback)
-- Mathlib.Algebra.Group.Submonoid.Units
/-- The equivalence between the top subgroup of `Mˣ` coerced to a submonoid `M` and the
units of `M`.  -/
Subgroup.ofUnitsTopEquiv : {M : Type u_1} → [inst : Monoid M] → ↥⊤.ofUnits ≃* Mˣ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_iff_neg_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] {a b : α},
  a + b < a ↔ b < 0
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.iIndepFun.mgf_sum : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X : ι → Ω → ℝ},
  ProbabilityTheory.iIndepFun X μ →
    (∀ (i : ι), Measurable (X i)) →
      ∀ (s : Finset ι), ProbabilityTheory.mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, ProbabilityTheory.mgf (X i) μ t
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAt.mem_domChart_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAt I J n f x), x ∈ h.domChart.source
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given a finite set `s`, the product of `f i / g i` over `i ∈ s` equals the product of `f i`
over `i ∈ s` divided by the product of `g i` over `i ∈ s`.  -/
finprod_mem_div_distrib : ∀ {α : Type u_1} {G : Type u_4} {s : Set α} [inst : DivisionCommMonoid G] (f g : α → G),
  s.Finite → ∏ᶠ (i : α) (_ : i ∈ s), f i / g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) / ∏ᶠ (i : α) (_ : i ∈ s), g i
-- Mathlib.MeasureTheory.Function.LpSeminorm.Trim
MeasureTheory.eLpNorm_trim_ae : ∀ {α : Type u_1} {ε : Type u_3} {m m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] (hm : m ≤ m0) {f : α → ε},
  MeasureTheory.AEStronglyMeasurable f (μ.trim hm) → MeasureTheory.eLpNorm f p (μ.trim hm) = MeasureTheory.eLpNorm f p μ
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.dist_pointReflection_fixed : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (x y : P),
  dist ((AffineIsometryEquiv.pointReflection 𝕜 x) y) x = dist y x
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.mk_coe : ∀ (z : UpperHalfPlane) (h : optParam (0 < (↑z).im) ⋯), { coe := ↑z, coe_im_pos := h } = z
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff edistances of `s` to `t` and of `t` to `s` coincide.  -/
Metric.hausdorffEDist_comm : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α}, Metric.hausdorffEDist s t = Metric.hausdorffEDist t s
-- Init.Data.Vector.Lemmas
Vector.eq_empty_of_size_eq_zero : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} (h : n = 0), xs = Vector.cast ⋯ #v[]
-- Mathlib.ModelTheory.Order
/-- The theory of dense linear orders is `ℵ₀`-complete.  -/
FirstOrder.Language.dlo_isComplete : FirstOrder.Language.order.dlo.IsComplete
-- Init.Data.Int.Order
Int.le_neg_iff : ∀ {x y : ℤ}, x ≤ -y ↔ y ≤ -x
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instPreadditive : {R : Type u} → [inst : Ring R] → CategoryTheory.Preadditive (ModuleCat R)
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
AlgebraicGeometry.geometricallyReduced_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.GeometricallyReduced f ↔ AlgebraicGeometry.geometrically AlgebraicGeometry.IsReduced f
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (m.insertMany l)[k]? = m[k]?
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.brecOn_4.go : {motive_1 : Lean.Elab.Term.Do.Code → Sort u} →
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
    {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
      {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
        {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
          {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u} →
            {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u} →
              (t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                ((t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t) →
                  ((t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                      Lean.Elab.Term.Do.Code.below_1 t → motive_2 t) →
                    ((t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                        Lean.Elab.Term.Do.Code.below_2 t → motive_3 t) →
                      ((t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                          Lean.Elab.Term.Do.Code.below_3 t → motive_4 t) →
                        ((t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                            Lean.Elab.Term.Do.Code.below_4 t → motive_5 t) →
                          ((t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) →
                              Lean.Elab.Term.Do.Code.below_5 t → motive_6 t) →
                            ((t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) →
                                Lean.Elab.Term.Do.Code.below_6 t → motive_7 t) →
                              motive_5 t ×' Lean.Elab.Term.Do.Code.below_4 t
-- Init.Data.UInt.Basic
instMulUInt64 : Mul UInt64
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.measurable_uniqueElim_cylinderEvents : ∀ {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] [inst : Unique ι], Measurable uniqueElim
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- Decomposition of a `R`-algebra homomorphism from `R[M]` by
its values on `F (single a 1)`.  -/
MonoidAlgebra.lift_unique : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (F : MonoidAlgebra R M →ₐ[R] A) (f : MonoidAlgebra R M),
  F f = f.coeff.sum fun a b => b • F (MonoidAlgebra.single a 1)
-- Batteries.Lean.PersistentHashSet
/-- Merge two `PersistentHashSet`s.
 -/
Lean.PersistentHashSet.merge : {α : Type u_1} →
  [inst : BEq α] →
    [inst_1 : Hashable α] → Lean.PersistentHashSet α → Lean.PersistentHashSet α → Lean.PersistentHashSet α
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- Isomorphism on `forgetToSheafModuleCat` when given isomorphic initial objects.  -/
SheafOfModules.forgetToSheafModuleCatOfIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) →
        (X Y : Cᵒᵖ) →
          (hX : CategoryTheory.Limits.IsInitial X) →
            (hY : CategoryTheory.Limits.IsInitial Y) →
              (φ : X ≅ Y) →
                SheafOfModules.forgetToSheafModuleCat R X hX ≅
                  (SheafOfModules.forgetToSheafModuleCat R Y hY).comp
                    (CategoryTheory.sheafCompose J (ModuleCat.restrictScalars (RingCat.Hom.hom (R.obj.map φ.hom))))
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_zero : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
  (v : AddValuation R Γ₀), v 0 = ⊤
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.minEntry_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t₁.isEmpty = false} (h : t₁.Equiv t₂), t₁.minEntry he = t₂.minEntry ⋯
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- The image of `ExteriorAlgebra.ιMulti R n` spans the `n`th exterior power, as a submodule
of the exterior algebra. See `exteriorPower.ιMulti_span_fixedDegree_of_span_eq_top` for a version
where we restrict to elements of the form `x₁ ∧ ⋯ ∧ xₙ` where the `xᵢ` belong to a spanning set.  -/
ExteriorAlgebra.ιMulti_span_fixedDegree : ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ),
  Submodule.span R (Set.range ⇑(ExteriorAlgebra.ιMulti R n)) = ⋀[R]^n M
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.normal_subgroupOf_commutator_sup : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G), (⁅H₁, H₂⁆.subgroupOf (H₁ ⊔ H₂)).Normal
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.comp_id : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N), f.comp (ZeroHom.id M) = f
-- Mathlib.Algebra.Homology.EulerCharacteristic
ComplexShape.eulerCharSignsUpInt_χ : ∀ (n : ℤ), ComplexShape.EulerCharSigns.χ (ComplexShape.up ℤ) n = n.negOnePow
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
/-- If the coproduct comparison map for `G` at `(X,Y)` is an isomorphism, then `G` preserves the
pair of `(X,Y)`.
 -/
CategoryTheory.Limits.PreservesColimitPair.of_iso_coprod_comparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct (G.obj X) (G.obj Y)]
  [i : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison G X Y)],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) G
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLE_comp_ofLE_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} (X Y Z : CategoryTheory.Subobject B) (h₁ : X ≤ Y)
  (h₂ : Y ≤ Z) {Z_1 : C} (h : CategoryTheory.Subobject.underlying.obj Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (X.ofLE Y h₁) (CategoryTheory.CategoryStruct.comp (Y.ofLE Z h₂) h) =
    CategoryTheory.CategoryStruct.comp (X.ofLE Z ⋯) h
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.exists_of_res_eq_of_qcqs_of_top : ∀ {X : AlgebraicGeometry.Scheme} [CompactSpace ↥X] [QuasiSeparatedSpace ↥X] {f g s : ↑(X.presheaf.obj (Opposite.op ⊤))},
  TopCat.Presheaf.restrictOpen f (X.basicOpen s) ⋯ = TopCat.Presheaf.restrictOpen g (X.basicOpen s) ⋯ →
    ∃ n, s ^ n * f = s ^ n * g
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.empty_eq : ∀ {n : ℕ}, Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.empty.toList = []
-- Std.Async.Timer
_private.Std.Async.Timer.0.Std.Async.Interval.ofNative.inj : ∀ {native native_1 : Std.Internal.UV.Timer}, { native := native } = { native := native_1 } → native = native_1
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mem_toSubmodule_iff : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] (x : M) (s : ClosedSubmodule R M), x ∈ ↑s ↔ x ∈ s
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsStronglyCocartesian.map.congr_simp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p p_1 : CategoryTheory.Functor 𝒳 𝒮) (e_p : p = p_1) {R S : 𝒮} {a b : 𝒳} (f f_1 : R ⟶ S) (e_f : f = f_1)
  (φ φ_1 : a ⟶ b) (e_φ : φ = φ_1) [inst_2 : p.IsStronglyCocartesian f φ] {S' : 𝒮} {b' : 𝒳} {g g_1 : S ⟶ S'}
  (e_g : g = g_1) {f' f'_1 : R ⟶ S'} (e_f' : f' = f'_1) (hf' : f' = CategoryTheory.CategoryStruct.comp f g)
  (φ' φ'_1 : a ⟶ b') (e_φ' : φ' = φ'_1) [inst_3 : p.IsHomLift f' φ'],
  CategoryTheory.Functor.IsStronglyCocartesian.map p f φ hf' φ' =
    CategoryTheory.Functor.IsStronglyCocartesian.map p_1 f_1 φ_1 ⋯ φ'_1
-- Mathlib.Analysis.LocallyConvex.WeakDual
LinearMap.toSeminorm_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 F] (f : F →ₗ[𝕜] 𝕜) (g : E →ₗ[𝕜] F),
  f.toSeminorm.comp g = (f ∘ₗ g).toSeminorm
-- Mathlib.Algebra.Regular.Opposite
isRegular_unop : ∀ {R : Type u_1} [inst : Mul R] {a : Rᵐᵒᵖ}, IsRegular (MulOpposite.unop a) ↔ IsRegular a
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.nullMeasurableSet_insert : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)] {a : α} {s : Set α},
  MeasureTheory.NullMeasurableSet (insert a s) μ ↔ MeasureTheory.NullMeasurableSet s μ
-- Mathlib.LinearAlgebra.Basis.Fin
/-- Let `b` be a basis for a submodule `N` of `M`. If `y : M` is linear independent of `N`
and `y` and `N` together span the whole of `M`, then there is a basis for `M`
whose basis vectors are given by `Fin.snoc b y`.  -/
Module.Basis.mkFinSnoc : {R : Type u_3} →
  {M : Type u_5} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {n : ℕ} →
            {N : Submodule R M} →
              Module.Basis (Fin n) R ↥N →
                (y : M) →
                  (∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) →
                    (∀ (z : M), ∃ c, z + c • y ∈ N) → Module.Basis (Fin (n + 1)) R M
-- Mathlib.LinearAlgebra.TensorProduct.Basis
/-- If `{ℬᵢ}` is a basis for the module `M`, then every elements of `x ∈ M ⊗ N` can be uniquely written
as `∑ᵢ ℬᵢ ⊗ nᵢ` for some `nᵢ ∈ N`.
 -/
TensorProduct.equivFinsuppOfBasisLeft : {R : Type u_1} →
  {M : Type u_3} →
    {N : Type u_4} →
      {ι : Type u_5} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R N] → [DecidableEq ι] → Module.Basis ι R M → TensorProduct R M N ≃ₗ[R] ι →₀ N
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Scalar multiplication distributes across addition  -/
DistribSMul.smul_add : ∀ {M : Type u_12} {A : Type u_13} {inst : AddZeroClass A} [self : DistribSMul M A] (a : M) (x y : A),
  a • (x + y) = a • x + a • y
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.addLeft_symm : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : SeparatelyContinuousAdd G] (a : G),
  (Homeomorph.addLeft a).symm = Homeomorph.addLeft (-a)
-- Mathlib.Logic.Denumerable
/-- If `α` and `β` are denumerable, then so is their sum.  -/
Denumerable.sum : {α : Type u_1} → {β : Type u_2} → [Denumerable α] → [Denumerable β] → Denumerable (α ⊕ β)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.UInt16.beq_eq_decide_eq : ∀ {a b : UInt16}, (a == b) = decide (a = b)
-- Mathlib.RingTheory.WittVector.Defs
/-- The polynomials used for defining repeated addition of the ring of Witt vectors.  -/
WittVector.wittNSMul : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℕ → ℕ → MvPolynomial (Fin 1 × ℕ) ℤ
-- Std.Http.Protocol.H1.Config
/-- Maximum number of leading empty lines (bare CRLF) to skip before a request-line
(RFC 9112 §2.2 robustness). Default: 8.
 -/
Std.Http.Protocol.H1.Config.maxLeadingEmptyLines : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.cons_eq_smul : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : Monoid.PushoutI.NormalWord d) (hmw : w.fstIdx ≠ some i)
  (hgr : g ∉ (φ i).range), Monoid.PushoutI.NormalWord.cons g w hmw hgr = (Monoid.PushoutI.of i) g • w
-- Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
/-- The infinite sum of strongly measurable functions is measurable, `HasSum` version.  -/
MeasureTheory.StronglyMeasurable.hasSum : ∀ {X : Type u_4} {E : Type u_5} {ι : Type u_6} [inst : MeasurableSpace X] [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [ContinuousAdd E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated]
  [TopologicalSpace.PseudoMetrizableSpace E] {f : ι → X → E} {g : X → E},
  (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
    (∀ (x : X), HasSum (fun i => f i x) (g x) L) → MeasureTheory.StronglyMeasurable g
-- Lean.Meta.IntInstTesters
Lean.Meta.DefEq.isInstDvdInt : Lean.Expr → Lean.MetaM Bool
-- Lean.MetavarContext
Lean.instantiateLCtxMVars : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.LocalContext → m Lean.LocalContext
-- Mathlib.Data.EReal.Operations
/-- For any extended real number `x`, the sum of `x` and `⊤` is equal to `⊤`
if and only if `x` is not `⊥`.  -/
EReal.add_top_iff_ne_bot : ∀ {x : EReal}, x + ⊤ = ⊤ ↔ x ≠ ⊥