mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_map_curry : ∀ {ι : Type u_6} {κ : Type u_7} {X : Type u_8} {mX : MeasurableSpace X} (μ : ι → κ → MeasureTheory.Measure X)
  [hμ : ∀ (i : ι) (j : κ), MeasureTheory.IsProbabilityMeasure (μ i j)],
  MeasureTheory.Measure.map (⇑(MeasurableEquiv.curry ι κ X)) (MeasureTheory.Measure.infinitePi fun p => μ p.1 p.2) =
    MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.infinitePi fun j => μ i j
-- Lean.Elab.ErrorUtils
_private.Lean.Elab.ErrorUtils.0.Lean.HasOxfordStrings.and : {α : Sort u_1} → [self : Lean.HasOxfordStrings✝ α] → α
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat : ∀ {X : AlgebraicGeometry.Scheme} [CompactSpace ↥X], AlgebraicGeometry.IsDominant X.toSpecΓ
-- Mathlib.Topology.UniformSpace.Basic
uniformity_comap : ∀ {α : Type ua} {β : Type ub} {x : UniformSpace β} (f : α → β),
  uniformity α = Filter.comap (Prod.map f f) (uniformity β)
-- Mathlib.Topology.Algebra.Monoid
ContinuousAdd.of_nhds_zero : ∀ {M : Type u} [inst : AddMonoid M] [inst_1 : TopologicalSpace M],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0) →
    (∀ (x₀ : M), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) →
      (∀ (x₀ : M), nhds x₀ = Filter.map (fun x => x + x₀) (nhds 0)) → ContinuousAdd M
-- Mathlib.Topology.MetricSpace.Cover
Metric.IsCover.singleton_of_ediam_le : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} {s : Set X} {x : X},
  Metric.ediam s ≤ ↑ε → x ∈ s → Metric.IsCover ε s {x}
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_conj : ∀ (x : ℂ), Complex.sin ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.sin x)
-- Init.Data.Rat.Lemmas
Rat.ceil.eq_1 : ∀ (a : ℚ), a.ceil = if a.den = 1 then a.num else a.num / ↑a.den + 1
-- Lean.Meta.Tactic.Replace
/-- Modify `mvarId` target type using `f`.
 -/
Lean.MVarId.modifyTarget : Lean.MVarId → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.MetaM Lean.MVarId
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.diam_univ : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β),
  Metric.diam Set.univ = Metric.diam Set.univ
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.smulLeftCLM_const : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F] (c : ℂ) (f : TemperedDistribution E F),
  (TemperedDistribution.smulLeftCLM F fun x => c) f = c • f
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Limits.instPreservesFilteredColimitsOfSizeForgetOrderEmbeddingCarrier : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u + 1, u + 1} (CategoryTheory.forget PartOrdEmb)
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.eval₂Hom_congr' : ∀ {R : Type u} {S : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] {f₁ f₂ : R →+* S}
  {g₁ g₂ : σ → S} {p₁ p₂ : MvPolynomial σ R},
  f₁ = f₂ →
    (∀ i ∈ p₁.vars, i ∈ p₂.vars → g₁ i = g₂ i) →
      p₁ = p₂ → (MvPolynomial.eval₂Hom f₁ g₁) p₁ = (MvPolynomial.eval₂Hom f₂ g₂) p₂
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
interUnionBalls.eq_1 : ∀ {α : Type u} (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → SetRel α α),
  interUnionBalls xs u V = ⋂ n, ⋃ m, ⋃ (_ : m ≤ u n), UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.sdiv_subset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s t : Set β} {u : Set α}, s /ₛ t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x /ₛ y ∈ u
-- Mathlib.Algebra.Lie.Submodule
/-- A morphism of Lie modules `f : M → M'` pushes forward Lie submodules of `M` to Lie submodules
of `M'`.  -/
LieSubmodule.map : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {M' : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : Module R M] →
                [inst_4 : LieRingModule L M] →
                  [inst_5 : AddCommGroup M'] →
                    [inst_6 : Module R M'] →
                      [inst_7 : LieRingModule L M'] → (M →ₗ⁅R,L⁆ M') → LieSubmodule R L M → LieSubmodule R L M'
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.hasZeroObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.Limits.HasZeroMorphisms C] (β : Type w),
  CategoryTheory.Limits.HasZeroObject (CategoryTheory.GradedObject β C)
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.prodMk_right : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (b : β),
  LipschitzWith 1 fun a => (a, b)
-- Mathlib.Tactic.Sat.FromLRAT
/-- The clause expression of type `Clause`  -/
Mathlib.Tactic.Sat.LClause.expr : Mathlib.Tactic.Sat.LClause → Lean.Expr
-- Mathlib.RingTheory.Valuation.Basic
ValuationClass.toMonoidWithZeroHomClass : ∀ {F : Type u_7} {R : outParam (Type u_5)} {Γ₀ : outParam (Type u_6)} {inst : LinearOrderedCommMonoidWithZero Γ₀}
  {inst_1 : Ring R} {inst_2 : FunLike F R Γ₀} [self : ValuationClass F R Γ₀], MonoidWithZeroHomClass F R Γ₀
-- Mathlib.Order.CompleteLattice.Chain
ChainClosure.below.union : ∀ {α : Type u_1} {r : α → α → Prop} {motive : (a : Set α) → ChainClosure r a → Prop} {s : Set (Set α)}
  (a : ∀ a ∈ s, ChainClosure r a),
  (∀ (a_1 : Set α) (a_2 : a_1 ∈ s), ChainClosure.below ⋯) →
    (∀ (a_1 : Set α) (a_2 : a_1 ∈ s), motive a_1 ⋯) → ChainClosure.below ⋯
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.cancel_counit_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : D} (f f' : X ⟶ e.functor.obj (e.inverse.obj Y)),
  CategoryTheory.CategoryStruct.comp f (e.counit.app Y) = CategoryTheory.CategoryStruct.comp f' (e.counit.app Y) ↔
    f = f'
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.instIsEquivalenceMapOfIsIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} [CategoryTheory.IsIso f],
  (CategoryTheory.Under.map f).IsEquivalence
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
isLittleO_log_rpow_nhdsGT_zero : ∀ {r : ℝ}, r < 0 → Real.log =o[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ r
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceNatAdd : Lean.Meta.Simp.DSimproc
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.Truncated.cosk.full : ∀ (n : ℕ), (SSet.Truncated.cosk n).Full
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.instInhabited.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  ArchimedeanClass.instInhabited = { default := ⊤ }
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.isEmpty_iff_isEmpty : ∀ {α : Type u} [inst : TopologicalSpace α], IsEmpty (ConnectedComponents α) ↔ IsEmpty α
-- Init.Data.List.Nat.InsertIdx
List.insertIdx_eraseIdx_of_ge : ∀ {α : Type u} {a : α} {i j : ℕ} {as : List α},
  i < as.length → i ≤ j → (as.eraseIdx i).insertIdx j a = (as.insertIdx (j + 1) a).eraseIdx i
-- Mathlib.Order.Category.Semilat
SemilatInfCat_dual_comp_forget_to_partOrd : SemilatInfCat.dual.comp (CategoryTheory.forget₂ SemilatSupCat PartOrd) =
  (CategoryTheory.forget₂ SemilatInfCat PartOrd).comp PartOrd.dual
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.frequently : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {p : β → Prop},
  Filter.Tendsto f l₁ l₂ → (∃ᶠ (x : α) in l₁, p (f x)) → ∃ᶠ (y : β) in l₂, p y
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Handles state transitions that are not due to a new token. If `nextToken?` is `none`, then there are
no more tokens to process, so all remaining transitions occur. If it is `some t`, then state
transitions only occur for token boundaries less than the `t`'s start.
 -/
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.HandleOverlapState.untilToken : Lean.Server.FileWorker.HandleOverlapState✝ →
  Option Lean.Server.FileWorker.AbsoluteLspSemanticToken → Lean.Server.FileWorker.HandleOverlapState✝
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.map.match_1.splitter : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3) →
      (X Y : CategoryTheory.WithTerminal C) →
        (f : X ⟶ Y) →
          ((a a_1 : C) →
              (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1) →
                motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_1) f) →
            ((a : C) →
                (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
                  motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x) →
              ((x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
                  motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x) →
                motive X Y f
-- Init.Grind.Norm
Lean.Grind.or_swap13 : ∀ (p q r : Prop), (p ∨ q ∨ r) = (r ∨ q ∨ p)
-- Mathlib.Order.Booleanisation
Booleanisation.lift_sup_lift : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (a b : α),
  Booleanisation.lift a ⊔ Booleanisation.lift b = Booleanisation.lift (a ⊔ b)
-- Init.Meta.Defs
/-- Which occurrences to rewrite -/
Lean.Meta.Rewrite.Config.occs : Lean.Meta.Rewrite.Config → Lean.Meta.Occurrences
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableWithinAt.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 g s x → DifferentiableWithinAt 𝕜 (f + g) s x
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_congr : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : Filter α},
  f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → (f₁ =o[𝕜; l] g₁ ↔ f₂ =o[𝕜; l] g₂)
-- Init.Data.FloatArray.Basic
/-- See comment at `forInUnsafe`  -/
FloatArray.foldlMUnsafe : {β : Type v} →
  {m : Type v → Type w} →
    [Monad m] → (β → Float → m β) → β → (as : FloatArray) → optParam ℕ 0 → optParam ℕ as.size → m β
-- Mathlib.CategoryTheory.Sites.Precoverage.Generates
CategoryTheory.Precoverage.Generates.le_toPrecoverage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {J : CategoryTheory.GrothendieckTopology C}, K.Generates J → K ≤ J.toPrecoverage
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.SurjectiveOnStalks f]
  [AlgebraicGeometry.SurjectiveOnStalks g],
  AlgebraicGeometry.SurjectiveOnStalks (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.liftCocone_pt : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J T) {X : T}
  (s : (CategoryTheory.Functor.const J).obj X ⟶ D) (c : CategoryTheory.Limits.Cocone D) (p : X ⟶ c.pt)
  (hp : ∀ (j : J), CategoryTheory.CategoryStruct.comp (s.app j) (c.ι.app j) = p),
  (CategoryTheory.Under.liftCocone D s c p hp).pt = CategoryTheory.Under.mk p
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.smul_oreDiv_one : ∀ {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] [inst_5 : IsScalarTower R M M]
  [inst_6 : IsScalarTower R M X] (r : R) (x : X), r • (x /ₒ 1) = r • x /ₒ 1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.imageMonoidHom.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] [inst_4 : FunLike F α β] [inst_5 : MonoidHomClass F α β] (f : F),
  Finset.imageMonoidHom f = { toFun := (Finset.imageMulHom f).toFun, map_one' := ⋯, map_mul' := ⋯ }
-- Init.Data.List.MinMax
List.min?_eq_none_iff : ∀ {α : Type u_1} {xs : List α} [inst : Min α], xs.min? = none ↔ xs = []
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.mem_iff_mem_rci : ∀ {α : Type u} {r : Std.Rii α} [inst : LE α] [inst_1 : Std.PRange.Least? α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxi.IsAlwaysFinite α] {a : α},
  a ∈ r ↔ a ∈ Std.PRange.UpwardEnumerable.least...*
-- Init.Data.Fin.Iterate
/-- `hIterate_eq`provides a mechanism for replacing `hIterate P s f` with a
function `state` showing that matches the steps performed by `hIterate`.

This allows rewriting incremental code using `hIterate` with a
non-incremental state function.
 -/
Fin.hIterate_eq : ∀ {P : ℕ → Sort u_1} (state : (i : ℕ) → P i) {n : ℕ} (f : (i : Fin n) → P ↑i → P (↑i + 1)) (s : P 0),
  s = state 0 → (∀ (i : Fin n), f i (state ↑i) = state (↑i + 1)) → Fin.hIterate P s f = state n
-- Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
/-- For any `p`, the power of `p` in `x^n` is `n` times the power in `x`  -/
factorization_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : NormalizationMonoid α]
  [inst_3 : DecidableEq α] {x : α} {n : ℕ}, factorization (x ^ n) = n • factorization x
-- Mathlib.Data.Vector.Basic
List.Vector.sum_set : ∀ {α : Type u_1} {n : ℕ} [inst : AddMonoid α] (v : List.Vector α n) (i : Fin n) (a : α),
  (v.set i a).toList.sum = (List.Vector.take (↑i) v).toList.sum + a + (List.Vector.drop (↑i + 1) v).toList.sum
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instReprOffset : Repr Std.Time.Hour.Offset
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'.d.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (i j : ι), HomologicalComplex.truncGE'.d K e i j = HomologicalComplex.truncGE'.d K e i j
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x))
      (Y.fromSpecResidueField (f x)) =
    CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) f
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.Context.mk.inj : ∀ {«meta» : Lean.Server.DocumentMeta} {cursorPos : Lean.Lsp.Position} {onGoal : Option ℕ}
  {stx : Option (Lean.TSyntax `tactic)} {masterToken statusToken solvedToken : ProofWidgets.RefreshToken}
  {goal : Lean.MVarId} {hyp? : Option Lean.FVarId} {pos : Lean.SubExpr.Pos} {meta_1 : Lean.Server.DocumentMeta}
  {cursorPos_1 : Lean.Lsp.Position} {onGoal_1 : Option ℕ} {stx_1 : Option (Lean.TSyntax `tactic)}
  {masterToken_1 statusToken_1 solvedToken_1 : ProofWidgets.RefreshToken} {goal_1 : Lean.MVarId}
  {hyp?_1 : Option Lean.FVarId} {pos_1 : Lean.SubExpr.Pos},
  { «meta» := «meta», cursorPos := cursorPos, onGoal := onGoal, stx := stx, masterToken := masterToken,
        statusToken := statusToken, solvedToken := solvedToken, goal := goal, hyp? := hyp?, pos := pos } =
      { «meta» := meta_1, cursorPos := cursorPos_1, onGoal := onGoal_1, stx := stx_1, masterToken := masterToken_1,
        statusToken := statusToken_1, solvedToken := solvedToken_1, goal := goal_1, hyp? := hyp?_1, pos := pos_1 } →
    «meta» = meta_1 ∧
      cursorPos = cursorPos_1 ∧
        onGoal = onGoal_1 ∧
          stx = stx_1 ∧
            masterToken = masterToken_1 ∧
              statusToken = statusToken_1 ∧ solvedToken = solvedToken_1 ∧ goal = goal_1 ∧ hyp? = hyp?_1 ∧ pos = pos_1
-- Mathlib.GroupTheory.Subgroup.Centralizer
/-- If all the elements of a set `s` commute, then `closure s` is a commutative group.  -/
Subgroup.isMulCommutative_closure : ∀ {G : Type u_1} [inst : Group G] {k : Set G},
  (∀ x ∈ k, ∀ y ∈ k, x * y = y * x) → IsMulCommutative ↥(Subgroup.closure k)
-- Mathlib.Order.Filter.Lift
Filter.lift_le : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Filter β} {h : Filter β} {s : Set α},
  s ∈ f → g s ≤ h → f.lift g ≤ h
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- Constructing an equivalence between `Nonempty (IsWeakLimit c)` and `Nonempty (IsWeakLimit d)`
from a natural isomorphism between the underlying functors, and then an isomorphism between `c`
transported along this and `d`.
 -/
CategoryTheory.Limits.IsWeakLimit.iff_of_natIso_of_iso : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F G : CategoryTheory.Functor J C} (α : F ≅ G)
  (c : CategoryTheory.Limits.Cone F) (d : CategoryTheory.Limits.Cone G)
  (w : (CategoryTheory.Limits.Cone.postcompose α.hom).obj c ≅ d),
  Nonempty (CategoryTheory.Limits.IsWeakLimit c) ↔ Nonempty (CategoryTheory.Limits.IsWeakLimit d)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.ediam_image : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (s : Set P),
  Metric.ediam (⇑f '' s) = Metric.ediam s
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.measure_mul_measure_eq : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] [MeasurableInv G]
  (μ' ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν']
  [μ'.IsMulLeftInvariant] [ν'.IsMulLeftInvariant] (s t : Set G), ν' s ≠ 0 → ν' s ≠ ⊤ → μ' s * ν' t = ν' s * μ' t
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.nat_mul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : NonAssocSemiring α],
  Function.Periodic f c → ∀ (n : ℕ), Function.Periodic f (↑n * c)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → γ a}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    ∀ (h : Std.Internal.List.containsKey k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) = true),
      Std.Internal.List.getValueCast k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) h =
        f k (Std.Internal.List.getValueCast k l ⋯)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- The sheaf of smooth functions from `M` to `G`, for `G` a Lie group, as a sheaf of
groups.  -/
smoothSheafGroup : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              ModelWithCorners 𝕜 EM HM →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [ChartedSpace HM M] →
                                  (G : Type u) →
                                    [inst_9 : TopologicalSpace G] →
                                      [inst_10 : ChartedSpace H G] →
                                        [inst_11 : Group G] → [LieGroup I (↑⊤) G] → TopCat.Sheaf GrpCat (TopCat.of M)
-- Mathlib.Analysis.Convex.Strict.Extreme
Set.extremePoints_Icc : ∀ {a b : ℝ}, a ≤ b → Set.extremePoints ℝ (Set.Icc a b) = {a, b}
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The short complex `K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)`.  -/
HomologicalComplex.sc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} → {c : ComplexShape ι} → HomologicalComplex C c → ι → CategoryTheory.ShortComplex C
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.homFromEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (g : Y ⟶ Z),
  α.homFromEquiv.symm g = CategoryTheory.CategoryStruct.comp α.hom g
-- Mathlib.Algebra.Order.Group.CompleteLattice
ciInf_add : ∀ {ι : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
  [AddRightMono G], BddBelow (Set.range f) → ∀ (a : G), (⨅ i, f i) + a = ⨅ i, f i + a
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.isMinOn_of_rightDeriv_eq_zero : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ}, ConvexOn ℝ S f → x ∈ interior S → derivWithin f (Set.Ioi x) x = 0 → IsMinOn f S x
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.mk : ∀ {S : Type u_3} {G : outParam (Type u_4)} [inst : SubNegMonoid G] [inst_1 : SetLike S G]
  [toAddSubmonoidClass : AddSubmonoidClass S G] [toNegMemClass : NegMemClass S G], AddSubgroupClass S G
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqnsExtState.mk.inj : ∀ {map : Lean.PHashMap Lean.Name Lean.Meta.Match.MatchEqns} {eqns : Lean.PHashSet Lean.Name}
  {map_1 : Lean.PHashMap Lean.Name Lean.Meta.Match.MatchEqns} {eqns_1 : Lean.PHashSet Lean.Name},
  { map := map, eqns := eqns } = { map := map_1, eqns := eqns_1 } → map = map_1 ∧ eqns = eqns_1
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.hermiteTheorem.boundOfDiscBdd.eq_1 : ∀ (N : ℕ),
  NumberField.hermiteTheorem.boundOfDiscBdd N = NNReal.sqrt ↑N * 2 ^ NumberField.hermiteTheorem.rankOfDiscrBdd N + 1
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_bot : ∀ {V : Type u} {v : V}, ⊥.neighborSet v = ∅
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- Being smooth is stable under composition.  -/
AlgebraicGeometry.instIsStableUnderCompositionSchemeSmooth : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.Smooth
-- Mathlib.RingTheory.Morita.Basic
IsMoritaEquivalent.symm : ∀ (R : Type u₀) [inst : CommSemiring R] {A : Type u₁} [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u₂}
  [inst_3 : Ring B] [inst_4 : Algebra R B], IsMoritaEquivalent R A B → IsMoritaEquivalent R B A
-- Mathlib.Algebra.Order.Ring.Abs
/-- If `n` is odd and `a` is even, then `n % a` is odd.  -/
Odd.mod_even : ∀ {n a : ℕ}, Odd n → Even a → Odd (n % a)
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.instResidueField : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Ideal S)
  [inst_3 : P.IsPrime] [Algebra.QuasiFinite R S], Algebra.QuasiFinite R P.ResidueField
-- Mathlib.Order.CompleteLattice.Basic
OrderIso.map_sInf_eq_sInf_symm_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β) (s : Set α),
  f (sInf s) = sInf (⇑f.symm ⁻¹' s)
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.u_support : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E],
  Function.support ExistsContDiffBumpBase.u = Metric.ball 0 1
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_toBitVec : ∀ (x : Int16), Int16.ofBitVec x.toBitVec = x