mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Polynomial.cyclotomic_eval_le_add_one_pow_totient : ∀ {q : ℝ}, 1 < q → ∀ (n : ℕ), Polynomial.eval q (Polynomial.cyclotomic n ℝ) ≤ (q + 1) ^ n.totient
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, panicking if the map is
empty.
 -/
Std.ExtDTreeMap.maxEntry! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → [Inhabited ((a : α) × β a)] → Std.ExtDTreeMap α β cmp → (a : α) × β a
-- Mathlib.Topology.Compactness.Compact
IsCompact.image : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
  IsCompact s → Continuous f → IsCompact (f '' s)
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.altitude.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.altitude i =
    AffineSubspace.mk' (s.points i) (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ ⊓ affineSpan ℝ (Set.range s.points)
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.rightDeriv_fderiv_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G) (x : G),
  φ.rightDeriv ((fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)) x) = x
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.coe_id : ∀ (R : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : Star A],
  ⇑(StarAlgHom.id R A) = id
-- Mathlib.Order.WithBot
WithTop.eq_bot_iff_forall_le : ∀ {α : Type u_1} [inst : PartialOrder α] [Nonempty α] [NoBotOrder α] {x : WithTop (WithBot α)},
  x = ⊥ ↔ ∀ (a : α), x ≤ ↑↑a
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.any_filterM : ∀ {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_2 : MonadLiftT m n] [inst_3 : Std.IteratorLoop α m m] [inst_4 : Monad m] [LawfulMonad m] [inst_6 : Monad n]
  [inst_7 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n]
  [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {f : β → n (ULift.{w, 0} Bool)} {p : β → Bool},
  Std.IterM.any p (Std.IterM.filterM f it) =
    Std.IterM.anyM
      (fun x => do
        let __do_lift ← f x
        if __do_lift.down = true then pure { down := p x } else pure { down := false })
      (Std.IterM.mapM pure it)
-- Init.Prelude
/-- Unsigned 64-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 64-bit value
rather than wrapping a `BitVec 64`.
 -/
UInt64 : Type
-- Mathlib.Analysis.Calculus.Implicit
/-- **Alias** of `ImplicitFunctionData.prodFun_implicitFunction`. -/
ImplicitFunctionData.prod_map_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  ∀ᶠ (p : F × G) in nhds (φ.prodFun φ.pt), φ.prodFun (φ.implicitFunction p.1 p.2) = p
-- Mathlib.Algebra.Category.MonCat.Limits
/-- (Internal use only; use the limits API.)  -/
AddMonCat.HasLimits.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddMonCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] → CategoryTheory.Limits.Cone F
-- Mathlib.GroupTheory.Coprod.Basic
/-- Lift two monoid equivalences `e : M ≃* N` and `e' : M' ≃* N'` to a monoid equivalence
`(M ∗ M') ≃* (N ∗ N')`.  -/
MulEquiv.coprodCongr : {M : Type u_1} →
  {N : Type u_2} →
    {M' : Type u_3} →
      {N' : Type u_4} →
        [inst : MulOneClass M] →
          [inst_1 : MulOneClass N] →
            [inst_2 : MulOneClass M'] →
              [inst_3 : MulOneClass N'] → M ≃* N → M' ≃* N' → Monoid.Coprod M M' ≃* Monoid.Coprod N N'
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.rank : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Module.finrank ℤ (NumberField.RingOfIntegers K) = Module.finrank ℚ K
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instSemigroup.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Semigroup M] [inst_2 : ContinuousMul M],
  SeparationQuotient.instSemigroup = { toMul := SeparationQuotient.instMul, mul_assoc := ⋯ }
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_smul_univ : ∀ {ι : Type u_7} {R : Type u_12} [inst : CommSemiring R] {M : Type u_13} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {N : Type u_14} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Fintype ι]
  (f : M [⋀^ι]→ₗ[R] N) (c : ι → R) (m : ι → M), (f fun i => c i • m i) = (∏ i, c i) • f m
-- Mathlib.Order.Interval.Finset.Defs
BddBelow.finite_of_bddAbove : ∀ {α : Type u_3} [inst : Preorder α] [LocallyFiniteOrder α] {s : Set α}, BddBelow s → BddAbove s → s.Finite
-- Mathlib.Data.Nat.GCD.Basic
Nat.dvd_lcm_of_dvd_right : ∀ {a b : ℕ}, a ∣ b → ∀ (c : ℕ), a ∣ c.lcm b
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.h : Std.Time.GenericFormat.DateBuilder✝ → Option (Std.Time.Internal.Bounded.LE 1 12)
-- Init.Data.Slice.List.Lemmas
ListSlice.mkSlice_ric_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : ListSlice α} {hi : ℕ},
  (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rco.Sliceable.mkSlice xs 0...hi + 1
-- Init.Data.Vector.Lemmas
Vector.forall_mem_ne : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n}, (∀ a' ∈ xs, ¬a = a') ↔ a ∉ xs
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (base : C)
  (fiber : ↑(F.obj base)) (base_1 : C) (fiber_1 : ↑(F.obj base_1)),
  ({ base := base, fiber := fiber } = { base := base_1, fiber := fiber_1 }) = (base = base_1 ∧ fiber ≍ fiber_1)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_reverse : ∀ (ctx : Nat.Internal.Linear.Context) (p : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.denote ctx (List.reverse p) = Nat.Internal.Linear.Poly.denote ctx p
-- Lean.Parser.Term
Lean.Parser.Term.explicitUniv.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Regular.IsSMulRegular
/-- Given a left exact sequence `0 → M → M' → M''`, if `r` is regular on both
`M` and `M''` it's regular `M'` too.  -/
isSMulRegular_of_range_eq_ker : ∀ {R : Type u_1} {M : Type u_3} {M' : Type u_4} {M'' : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] [inst_5 : AddCommGroup M'']
  [inst_6 : Module R M''] {r : R} {f : M →ₗ[R] M'} {g : M' →ₗ[R] M''},
  Function.Injective ⇑f → f.range = g.ker → IsSMulRegular M r → IsSMulRegular M'' r → IsSMulRegular M' r
-- Lean.Expr
Lean.Expr.fvar.injEq : ∀ (fvarId fvarId_1 : Lean.FVarId), (Lean.Expr.fvar fvarId = Lean.Expr.fvar fvarId_1) = (fvarId = fvarId_1)
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Algebra.IsAlgebraic.isTranscendenceBasis_of_lift_le_trdeg_of_finite : ∀ {ι : Type u} (R : Type u_1) {A : Type w} (x : ι → A) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [NoZeroDivisors A] [FaithfulSMul R A] [Finite ι] [alg : Algebra.IsAlgebraic (↥(Algebra.adjoin R (Set.range x))) A],
  Cardinal.lift.{w, u} (Cardinal.mk ι) ≤ Cardinal.lift.{u, w} (Algebra.trdeg R A) → IsTranscendenceBasis R x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE!_eq_get!_getEntryGE? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α}
  [inst_1 : Inhabited ((a : α) × β a)],
  Std.DTreeMap.Internal.Impl.getEntryGE! k t = (Std.DTreeMap.Internal.Impl.getEntryGE? k t).get!
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundaries₁_ext_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{max u u_1, u, u} k G}
  {f₁ f₂ : ↥(groupCohomology.coboundaries₁ A)}, f₁ = f₂ ↔ ∀ (g : G), f₁ g = f₂ g
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.ofFractionRing_add : ∀ {K : Type u} [inst : CommRing K] (p q : FractionRing (Polynomial K)),
  { toFractionRing := p + q } = { toFractionRing := p } + { toFractionRing := q }
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
/-- The property that the cardinal of a type `X : Type u` is less than `κ : Cardinal.{v}`.  -/
HasCardinalLT : Type u → Cardinal.{v} → Prop
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.isStrictMinor_iff_isMinor_ne : ∀ {α : Type u_1} {M N : Matroid α}, N <m M ↔ N ≤m M ∧ N ≠ M
-- Init.Notation
Lean.guardMsgsFilterSeverity : Lean.ParserDescr
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.coneEquiv_unitIso_hom_app_hom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)} (X_1 : CategoryTheory.Limits.Cone K),
  (CategoryTheory.WithTerminal.coneEquiv.unitIso.hom.app X_1).hom.left = CategoryTheory.CategoryStruct.id X_1.pt.left
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.symm_ne : ∀ {V : Type u_1} {G : SimpleGraph V} (d : G.Dart), d.symm ≠ d
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- Additive submonoid closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure s ≤ closure t`.  -/
AddSubmonoid.closure_mono : ∀ {M : Type u_1} [inst : AddZeroClass M] ⦃s t : Set M⦄, s ⊆ t → AddSubmonoid.closure s ≤ AddSubmonoid.closure t
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.ext : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (L₁' L₂' : LieSubalgebra R L), (∀ (x : L), x ∈ L₁' ↔ x ∈ L₂') → L₁' = L₂'
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.isDiameter_iff_mem_and_mem_and_dist : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.ordered_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  List.Pairwise (fun a b => cmp a b = Ordering.lt) t.toList
-- Init.Data.Option.Instances
/-- Given a function from the elements of `α` that satisfy `p` to `β` and a proof that an optional value
satisfies `p` if it's present, applies the function to the value.

Examples:
```lean example
def attach (v : Option α) : Option { y : α // v = some y } :=
  v.pmap (fun a (h : a ∈ v) => ⟨_, h⟩) (fun _ h => h)
```
```lean example
#reduce attach (some 3)
```
```output
some ⟨3, ⋯⟩
```
```lean example
#reduce attach none
```
```output
none
```
 -/
Option.pmap : {α : Type u_1} →
  {β : Type u_2} → {p : α → Prop} → ((a : α) → p a → β) → (o : Option α) → (∀ (a : α), o = some a → p a) → Option β
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.ObjectProperty.map_top : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D), ⊤.map F = F.essImage
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Two morphisms out of a universal `T`-structured arrow are equal if their image under `T` are
equal after precomposing the universal arrow.  -/
CategoryTheory.StructuredArrow.IsUniversal.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal) {c : C}
  {η η' : f.right ⟶ c},
  CategoryTheory.CategoryStruct.comp f.hom (T.map η) = CategoryTheory.CategoryStruct.comp f.hom (T.map η') → η = η'
-- Mathlib.Data.Finset.Image
/-- **Alias** of the forward direction of `Finset.mapsTo_iff_image_subset`. -/
Set.MapsTo.finsetImage_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β},
  Set.MapsTo f ↑s ↑t → Finset.image f s ⊆ t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.some_ne_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {x y : R} (h : W'.Nonsingular x y),
  WeierstrassCurve.Affine.Point.some x y h ≠ 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_insertList_of_contains_eq_false_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α},
  Std.Internal.List.containsKey k toInsert = false →
    Std.Internal.List.getValue? k (Std.Internal.List.insertList l toInsert) = Std.Internal.List.getValue? k l
-- Mathlib.Data.Matrix.Mul
Matrix.intCast_mulVec : ∀ {m : Type u_2} {α : Type v} [inst : NonAssocRing α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] (x : ℤ) (v : m → α),
  (↑x).mulVec v = ↑x • v
-- Mathlib.Algebra.Category.Ring.Limits
RingCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget RingCat)
-- Init.Data.BitVec.Lemmas
BitVec.pow_zero : ∀ {w : ℕ} {x : BitVec w}, x ^ 0 = 1#w
-- Mathlib.Algebra.Ring.Periodic
Multiset.periodic_sum : ∀ {α : Type u_1} {β : Type u_2} {c : α} [inst : Add α] [inst_1 : AddCommMonoid β] (s : Multiset (α → β)),
  (∀ f ∈ s, Function.Periodic f c) → Function.Periodic s.sum c
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_comp_rid_symm_assoc : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid P]
  [inst_6 : Module R P] (f : P →ₗ[R] TensorProduct R M N),
  ↑(TensorProduct.assoc R M N R) ∘ₗ ↑(TensorProduct.rid R (TensorProduct R M N)).symm ∘ₗ f =
    TensorProduct.map LinearMap.id ↑(TensorProduct.rid R N).symm ∘ₗ f
-- Mathlib.Analysis.Calculus.Deriv.Abs
hasStrictDerivAt_abs_neg : ∀ {x : ℝ}, x < 0 → HasStrictDerivAt (fun x => |x|) (-1) x
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_eq_right : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x \ y = y ↔ x = ⊥ ∧ y = ⊥
-- Init.Data.SInt.Bitwise
ISize.not_zero : ~~~0 = -1
-- Std.Data.DHashMap.Lemmas
/-- Simpler variant of `get!_filterMap` when `LawfulBEq` is available.  -/
Std.DHashMap.Const.get!_filterMap' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  [inst : Inhabited γ] {f : α → β → Option γ} {k : α},
  Std.DHashMap.Const.get! (Std.DHashMap.filterMap f m) k = ((Std.DHashMap.Const.get? m k).bind (f k)).get!
-- Std.Internal.Do.WP.Basic
/-- Soundness for `Except`: if `wp prog P` holds, then `P` holds of the result.  -/
Std.Internal.Do.Except.of_wp_eq : ∀ {ε α : Type} {x prog : Except ε α},
  prog = x →
    ∀ (P : Except ε α → Prop),
      Std.Internal.Do.wp prog (fun a => P (Except.ok a)) epost⟨fun e => P (Except.error e)⟩ → P x
-- Batteries.Data.List.Basic
/-- `pwFilter R l` is a maximal sublist of `l` which is `Pairwise R`.
`pwFilter (·≠·)` is the erase duplicates function (cf. `eraseDups`), and `pwFilter (·<·)` finds
a maximal increasing subsequence in `l`. For example,
```
pwFilter (·<·) [0, 1, 5, 2, 6, 3, 4] = [0, 1, 2, 3, 4]
```
 -/
List.pwFilter : {α : Type u_1} → (R : α → α → Prop) → [DecidableRel R] → List α → List α
-- Init.Data.Int.Linear
Int.Internal.Linear.of_not_dvd : ∀ (a b : ℤ), (a != 0) = true → ¬a ∣ b → b % a > 0
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.funCongrLeft_symm : ∀ (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} (e : m ≃ n), (LinearEquiv.funCongrLeft R M e).symm = LinearEquiv.funCongrLeft R M e.symm
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.toAddSubgroup : {G : Type u_1} → [inst : AddGroup G] → FiniteIndexNormalAddSubgroup G → AddSubgroup G
-- Mathlib.Topology.UniformSpace.CompactConvergence
ContinuousMap.uniformSpace_eq_iInf_precomp_of_cover : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {ι : Type u₃} {δ : ι → Type u_1}
  [inst_2 : (i : ι) → TopologicalSpace (δ i)] (φ : (i : ι) → C(δ i, α)),
  (∀ (i : ι), IsProperMap ⇑(φ i)) →
    (LocallyFinite fun i => Set.range ⇑(φ i)) →
      ⋃ i, Set.range ⇑(φ i) = Set.univ → inferInstance = ⨅ i, UniformSpace.comap (fun x => x.comp (φ i)) inferInstance
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.π'_f_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.ProjectiveResolution X),
  R.π'.f 0 =
    CategoryTheory.CategoryStruct.comp
      (R.cochainComplexXIso 0 0 CategoryTheory.ProjectiveResolution.π'_f_zero._proof_2).hom
      (CategoryTheory.CategoryStruct.comp (R.π.f 0) (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.univ_pi_Iio_ae_eq_Iic : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NullSingletonClass (μ i)] {f : (i : ι) → α i},
  (Set.univ.pi fun i => Set.Iio (f i)) =ᵐ[MeasureTheory.Measure.pi μ] Set.Iic f
-- Mathlib.Topology.Connected.TotallyDisconnected
Continuous.image_eq_of_connectedComponent_eq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [TotallyDisconnectedSpace β]
  {f : α → β}, Continuous f → ∀ (a b : α), connectedComponent a = connectedComponent b → f a = f b
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- The affine homeomorphism given by `p' ↦ p -ᵥ p'`. This is `Equiv.constVSub` as a
`ContinuousAffineEquiv`.  -/
ContinuousAffineEquiv.constVSub : (k : Type u_1) →
  {P₁ : Type u_2} →
    {V₁ : Type u_6} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] →
          [inst_2 : Module k V₁] →
            [inst_3 : AddTorsor V₁ P₁] →
              [inst_4 : TopologicalSpace P₁] →
                [inst_5 : TopologicalSpace V₁] → [IsTopologicalAddTorsor P₁] → P₁ → P₁ ≃ᴬ[k] V₁
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Reify.0.Lean.Meta.Grind.Arith.Linear.reify?.processSMul : ℕ →
  Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.Arith.Linear.LinearM (Option Lean.Meta.Grind.Arith.Linear.LinExpr)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Construct a `NormalExpr` expression from a Lean expression for an atomic 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.ofAtomM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
      [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] →
        [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
          Mathlib.Tactic.BicategoryLike.Atom → m Mathlib.Tactic.BicategoryLike.NormalExpr
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.associator_inv : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (X Y Z : C),
  (CategoryTheory.MonoidalCategoryStruct.associator
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
        (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) Y Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) X
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map
            (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε)
              (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight
              (CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) X
                Y)
              ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)))))
-- Mathlib.Tactic.ClickSuggestions.Apply
/-- The new goals.  -/
Mathlib.Tactic.ClickSuggestions.ApplyKey.newGoals : Mathlib.Tactic.ClickSuggestions.ApplyKey → Array Lean.Meta.AbstractMVarsResult
-- Mathlib.Algebra.Order.Monovary
Monovary.div_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {f₁ f₂ : ι → α} {g : ι → β}, Monovary f₁ g → Antivary f₂ g → Monovary (f₁ / f₂) g
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_succ_succ : ∀ {m n : ℤ}, ((m + 1)<...=n + 1).toList = List.map (fun x => x + 1) (m<...=n).toList
-- Init.Data.String.Substring
/-- Returns the starting position of the common prefix, working down from `spos, tpos`.  -/
_private.Init.Data.String.Substring.0.Substring.Raw.commonSuffix.loop : Substring.Raw → Substring.Raw → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Order.Filter.AtTopBot.Group
/-- $\lim_{x\to-\infty}|x|=+\infty$  -/
Filter.tendsto_abs_atBot_atTop : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G],
  Filter.Tendsto abs Filter.atBot Filter.atTop
-- Mathlib.Topology.Algebra.Order.Support
HasCompactSupport.inf : ∀ {X : Type u_1} {M : Type u_2} [inst : TopologicalSpace X] [inst_1 : Zero M] [inst_2 : SemilatticeInf M] {f g : X → M},
  HasCompactSupport f → HasCompactSupport g → HasCompactSupport (f ⊓ g)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
continuousOn_extChartAt_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M),
  ContinuousOn (↑(extChartAt I x).symm) (extChartAt I x).target
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionResult.subgoal.inj : ∀ {mvarId : Lean.MVarId} {newEqs : Array Lean.FVarId} {remainingNames : List Lean.Name} {mvarId_1 : Lean.MVarId}
  {newEqs_1 : Array Lean.FVarId} {remainingNames_1 : List Lean.Name},
  Lean.Meta.InjectionResult.subgoal mvarId newEqs remainingNames =
      Lean.Meta.InjectionResult.subgoal mvarId_1 newEqs_1 remainingNames_1 →
    mvarId = mvarId_1 ∧ newEqs = newEqs_1 ∧ remainingNames = remainingNames_1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_diff_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ \ m₂)[k]? = m₁[k]?