mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Convenient.GeneratedBy
/-- The `X`-generated topology is also coinduced by a single map out of a sigma type.  -/
TopologicalSpace.generatedBy_eq_coinduced : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y],
  TopologicalSpace.generatedBy X = TopologicalSpace.coinduced (fun x => x.fst.snd x.snd) inferInstance
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizer.isoTargetOfSelf_hom : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y),
  (CategoryTheory.Limits.coequalizer.isoTargetOfSelf f).hom =
    CategoryTheory.Limits.coequalizer.desc (CategoryTheory.CategoryStruct.id Y) ⋯
-- Mathlib.Data.Fintype.Pi
Set.forall_finite_image_eval_iff : ∀ {δ : Type u_3} [Finite δ] {κ : δ → Type u_4} {s : Set ((d : δ) → κ d)},
  (∀ (d : δ), (Function.eval d '' s).Finite) ↔ s.Finite
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
multipliable_extend_one : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {g : β → γ}, Function.Injective g → (Multipliable (Function.extend g f 1) ↔ Multipliable f)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.mulR.sizeOf_spec : ∀ (a : Nat.Internal.Linear.Expr) (k : ℕ), sizeOf (a.mulR k) = 1 + sizeOf a + sizeOf k
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.coe_liftAlgHom : ∀ {A : Type u_4} [inst : CommSemiring A] {R : Type u_5} [inst_1 : CommSemiring R] [inst_2 : Algebra A R]
  {M : Submonoid R} {S : Type u_6} [inst_3 : CommSemiring S] [inst_4 : Algebra A S] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower A R S] {P : Type u_7} [inst_7 : CommSemiring P] [inst_8 : Algebra A P]
  [inst_9 : IsLocalization M S] {f : R →ₐ[A] P} (hf : ∀ (y : ↥M), IsUnit (f ↑y)),
  ⇑(IsLocalization.liftAlgHom hf) = ⇑(IsLocalization.lift hf)
-- Mathlib.Order.RelIso.Set
RelHomClass.map_sup : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : SemilatticeSup α] [inst_1 : LinearOrder β]
  [inst_2 : FunLike F β α] [RelHomClass F (fun x1 x2 => x1 > x2) fun x1 x2 => x1 > x2] (a : F) (m n : β),
  a (max m n) = a m ⊔ a n
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
/-- `F.LaxLinear C` equips `F : D ⥤ D'` with a family of morphisms
`μₗ F : ∀ (c : C) (d : D), c ⊙ₗ F.obj d ⟶ F.obj (c ⊙ₗ d)`
that is natural in each variable and coherent with respect to left actions
of `C` on `D` and `D'`.  -/
CategoryTheory.Functor.LaxRightLinear : {D : Type u_1} →
  {D' : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] →
        CategoryTheory.Functor D D' →
          (C : Type u_3) →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.MonoidalCategory C] →
                [CategoryTheory.MonoidalCategory.MonoidalRightAction C D] →
                  [CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] → Type (max (max u_1 u_3) v_2)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivWithinAt.list_prod' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_5} {𝔸 : Type u_6} [inst_3 : NormedRing 𝔸]
  [inst_4 : NormedAlgebra 𝕜 𝔸] {f : ι → E → 𝔸} {f' : ι → E →L[𝕜] 𝔸} {l : List ι} {x : E},
  (∀ i ∈ l, HasFDerivWithinAt (fun x => f i x) (f' i) s x) →
    HasFDerivWithinAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod)
      (∑ i,
        (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod •
          MulOpposite.op (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod • f' l[i])
      s x
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullback i i]
  [inst_3 : CategoryTheory.Limits.HasPullback f g]
  [inst_4 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
  [inst_5 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
      (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
        (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).hom
      (CategoryTheory.Limits.pullback.fst f g) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i)
        (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
          (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f i)
        (CategoryTheory.CategoryStruct.comp g i))
-- Mathlib.Topology.Order.T5
Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhds : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a : X} {s t : Set X},
  Disjoint s (closure t) → a ∈ s → (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ nhds a
-- Mathlib.Order.RelIso.Set
RelIso.range_eq : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s), Set.range ⇑e = Set.univ
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.InvariantForm.apply_reflection_reflection : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (B : P.InvariantForm)
  (i : ι) (x y : M), (B.form ((P.reflection i) x)) ((P.reflection i) y) = (B.form x) y
-- Mathlib.SetTheory.Ordinal.Notation
/-- Multiplication of ordinal notations (correct only for normal input)  -/
ONote.mul : ONote → ONote → ONote
-- Mathlib.CategoryTheory.Localization.StructuredArrow
CategoryTheory.Localization.Construction.wInv.congr_simp : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (w w_1 : X ⟶ Y) (e_w : w = w_1) (hw : W w),
  CategoryTheory.Localization.Construction.wInv w hw = CategoryTheory.Localization.Construction.wInv w_1 ⋯
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_eq_zero_iff_degree_le_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.natDegree = 0 ↔ p.degree ≤ 0
-- Mathlib.Topology.Algebra.Monoid.Defs
Filter.tendsto_of_div_tendsto_one : ∀ {α : Type u_2} {E : Type u_3} [inst : CommGroup E] [inst_1 : TopologicalSpace E] [ContinuousMul E] {f g : α → E}
  (m : E) {x : Filter α}, Filter.Tendsto f x (nhds m) → Filter.Tendsto (g / f) x (nhds 1) → Filter.Tendsto g x (nhds m)
-- Std.Time.Internal.UnitVal
Std.Time.Internal.UnitVal.instOfNat : {α : ℚ} → {n : ℕ} → OfNat (Std.Time.Internal.UnitVal α) n
-- Mathlib.Analysis.Complex.ValueDistribution.Cartan
/-- Circle integrability of the term `fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖` that
appears in Cartan's formula.
 -/
ValueDistribution.circleIntegrable_log_meromorphicTrailingCoeffAt : ∀ {f : ℂ → ℂ}, CircleIntegrable (fun a => Real.log ‖meromorphicTrailingCoeffAt (fun x => f x - a) 0‖) 0 1
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cocone F} {t : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (w : F ≅ G),
  P.coconePointsIsoOfNatIso Q w = { hom := P.map t w.hom, inv := Q.map s w.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.ColimitCocone.mk.inj : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Functor J C} {cocone : CategoryTheory.Limits.Cocone F}
  {isColimit : CategoryTheory.Limits.IsColimit cocone} {cocone_1 : CategoryTheory.Limits.Cocone F}
  {isColimit_1 : CategoryTheory.Limits.IsColimit cocone_1},
  { cocone := cocone, isColimit := isColimit } = { cocone := cocone_1, isColimit := isColimit_1 } →
    cocone = cocone_1 ∧ isColimit ≍ isColimit_1
-- Mathlib.Topology.Category.Profinite.Basic
/-- The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus  -/
Profinite.toProfiniteAdjToCompHaus : CompHaus.toProfinite ⊣ profiniteToCompHaus
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_le_rpow_of_exponent_ge : ∀ {x : ENNReal} {y z : ℝ}, x ≤ 1 → z ≤ y → x ^ y ≤ x ^ z
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.brecOn_1.go : {motive_1 : Lean.Elab.InfoTree → Sort u} →
  {motive_2 : Lean.PersistentArray Lean.Elab.InfoTree → Sort u} →
    {motive_3 : Lean.PersistentArrayNode Lean.Elab.InfoTree → Sort u} →
      {motive_4 : Array Lean.Elab.InfoTree → Sort u} →
        {motive_5 : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u} →
          {motive_6 : List Lean.Elab.InfoTree → Sort u} →
            {motive_7 : List (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u} →
              (t : Lean.PersistentArray Lean.Elab.InfoTree) →
                ((t : Lean.Elab.InfoTree) → t.below → motive_1 t) →
                  ((t : Lean.PersistentArray Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_1 t → motive_2 t) →
                    ((t : Lean.PersistentArrayNode Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_2 t → motive_3 t) →
                      ((t : Array Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_3 t → motive_4 t) →
                        ((t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                            Lean.Elab.InfoTree.below_4 t → motive_5 t) →
                          ((t : List Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_5 t → motive_6 t) →
                            ((t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                                Lean.Elab.InfoTree.below_6 t → motive_7 t) →
                              motive_2 t ×' Lean.Elab.InfoTree.below_1 t
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.stabilizerEquivStabilizer_apply : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g : G} {a b : α} (hg : b = g • a)
  (x : ↥(MulAction.stabilizer G a)), ↑((MulAction.stabilizerEquivStabilizer hg) x) = (MulAut.conj g) ↑x
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
/-- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is a Dedekind domain,
the integral closure of `A` in `L` is a Dedekind domain.

This cannot be an instance since `K` can't be inferred. See also the instance
`integralClosure.isDedekindDomain_fractionRing` where `K := FractionRing A`.  -/
integralClosure.isDedekindDomain : ∀ (A : Type u_1) (K : Type u_2) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  (L : Type u_3) [inst_4 : Field L] [inst_5 : Algebra K L] [inst_6 : Algebra A L] [IsScalarTower A K L]
  [FiniteDimensional K L] [IsDomain A] [Algebra.IsSeparable K L] [IsDedekindDomain A],
  IsDedekindDomain ↥(integralClosure A L)
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- The map `g` from `V` to `V₂` corresponding to a map `f` from `P` to `P₂`, at a base point `p`,
is an isometry if `f` is one.  -/
AffineIsometryEquiv.vadd_vsub : ∀ {𝕜 : 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] [NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P]
  [inst_5 : SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [inst : PseudoMetricSpace P₂] [inst_6 : NormedAddTorsor V₂ P₂]
  {f : P → P₂}, Isometry f → ∀ {p : P} {g : V → V₂}, (∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p) → Isometry g
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.isInvalidContinuationByte.eq_1 : ∀ (b : UInt8), ByteArray.utf8DecodeChar?.isInvalidContinuationByte b = (b &&& 192 != 128)
-- Lean.Data.Lsp.Internal
/-- Definition site of the reference. May be `none` when we cannot find a definition site.  -/
Lean.Lsp.RefInfo.definition? : Lean.Lsp.RefInfo → Option Lean.Lsp.RefInfo.Location
-- Mathlib.Topology.Algebra.Monoid
GroupWithZero.isOpen_singleton_zero : ∀ {M : Type u_3} [inst : GroupWithZero M] [inst_1 : TopologicalSpace M] [ContinuousMul M] [CompactSpace M] [T1Space M],
  IsOpen {0}
-- Mathlib.RingTheory.WittVector.Identities
WittVector.verschiebung_frobenius : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] (x : WittVector p R),
  WittVector.verschiebung (WittVector.frobenius x) = x * ↑p
-- Lean.Syntax
Lean.Syntax.reprint : Lean.Syntax → Option String
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.greatestFib_lt : ∀ {m n : ℕ}, m.greatestFib < n ↔ m < Nat.fib n
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.op_vadd_set_vadd_eq_vadd_vadd_set : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd αᵃᵒᵖ β] [inst_1 : VAdd β γ] [inst_2 : VAdd α γ] (a : α)
  (s : Set β) (t : Set γ),
  (∀ (a : α) (b : β) (c : γ), (AddOpposite.op a +ᵥ b) +ᵥ c = b +ᵥ a +ᵥ c) → (AddOpposite.op a +ᵥ s) +ᵥ t = s +ᵥ a +ᵥ t
-- Init.Data.List.Lemmas
List.eq_getElem_of_length_eq_three : ∀ {α : Type u_1} (l : List α) (hl : l.length = 3), l = [l[0], l[1], l[2]]
-- Mathlib.Topology.Sheaves.Sheafify
/-- The local predicate on functions into the stalks,
asserting that the function is locally equal to a germ.
 -/
TopCat.Presheaf.Sheafify.isLocallyGerm : {X : TopCat} → (F : TopCat.Presheaf (Type v) X) → TopCat.LocalPredicate fun x => F.stalk x
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.isHomeomorph : ∀ {S : Type u_1} [inst : Semiring S] {S₁ : Type u_6} {M : Type u_7} {M₁ : Type u_8} [inst_1 : Semiring S₁]
  {σ : S →+* S₁} {σ' : S₁ →+* S} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ]
  [inst_4 : TopologicalSpace M] [inst_5 : AddCommMonoid M] [inst_6 : Module S M] [inst_7 : TopologicalSpace M₁]
  [inst_8 : AddCommMonoid M₁] [inst_9 : Module S₁ M₁] (f : M ≃SL[σ] M₁), IsHomeomorph ⇑f
-- Mathlib.Topology.UniformSpace.ProdApproximation
ContinuousMap.prodMul_def : ∀ {X : Type u_5} {Y : Type u_6} {R : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] (f : C(X, R)) (g : C(Y, R)),
  (ContinuousMap.prodMul f) g = f.comp ContinuousMap.fst * g.comp ContinuousMap.snd
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algHom_ext : ∀ {R : Type u_1} {A : Type u_2} {L : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring L] [inst_3 : Semiring B] (W : Submonoid A) [inst_4 : Algebra A L] [IsLocalization W L]
  [inst_6 : Algebra R A] [inst_7 : Algebra R L] [inst_8 : IsScalarTower R A L] [inst_9 : Algebra R B] {f g : L →ₐ[R] B},
  f.comp (Algebra.algHom R A L) = g.comp (Algebra.algHom R A L) → f = g
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.toList_foldr_inf_mem : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {p : T.CompleteType α}
  {t : Finset (L.withConstants α).Sentence}, List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ t.toList ∈ p ↔ ↑t ⊆ ↑p
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Real.Angle.arg_toCircle : ∀ (θ : Real.Angle), ↑(↑θ.toCircle).arg = θ
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_eq_head!_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.min! = t.toList.head!
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_sub : ∀ {x : ENNReal} (y z : ℝ), x ≠ 0 → x ≠ ⊤ → x ^ (y - z) = x ^ y / x ^ z
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorCompIsoId_zero_zero_inv_app : ∀ {C : Type u} (A : Type u_1) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (X : C),
  (CategoryTheory.shiftFunctorCompIsoId C 0 0 ⋯).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C A).inv.app X)
      ((CategoryTheory.shiftFunctor C 0).map ((CategoryTheory.shiftFunctorZero C A).inv.app X))
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.ofSpan_subset : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  (hs : ⊤ ≤ Submodule.span K s), Set.range ⇑(Module.Basis.ofSpan hs) ⊆ s
-- Mathlib.Tactic.Translate.Core
/-- The given name of the target: an anonymous name means no explicit name was provided,
and the translate tactic auto-generates a name instead  -/
Mathlib.Tactic.Translate.Config.target : Mathlib.Tactic.Translate.Config → Lean.Name
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_apply : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] (s : Set α) (f : α → M) (a : α) [inst_1 : Decidable (a ∈ s)],
  s.mulIndicator f a = if a ∈ s then f a else 1
-- Init.Data.Vector.Range
Vector.zipIdx_map : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {k : ℕ},
  (Vector.map f xs).zipIdx k = Vector.map (Prod.map f id) (xs.zipIdx k)
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
/-- The homeomorphism `homeomorphUnitSphereProd E` sends an additive Haar measure `μ`
to the product of `μ.toSphere` and `MeasureTheory.Measure.volumeIoiPow (dim E - 1)`,
where `dim E = Module.finrank ℝ E` is the dimension of `E`.  -/
MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  MeasureTheory.MeasurePreserving (⇑(homeomorphUnitSphereProd E)) (MeasureTheory.Measure.comap Subtype.val μ)
    (μ.toSphere.prod (MeasureTheory.Measure.volumeIoiPow (Module.finrank ℝ E - 1)))
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.whiskerLeft_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n m : ℕ} (F : CategoryTheory.ComposableArrows C m)
  (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) {X Y : Fin (n + 1)} (f : X ⟶ Y),
  (F.whiskerLeft Φ).map f = F.map (Φ.map f)
-- Mathlib.NumberTheory.Fermat
/-- Prime factors of `a ^ (2 ^ n) + 1` are of form `k * 2 ^ (n + 1) + 1`.  -/
Nat.pow_pow_add_primeFactors_one_lt : ∀ {a n p : ℕ}, Nat.Prime p → p ≠ 2 → p ∣ a ^ 2 ^ n + 1 → ∃ k, p = k * 2 ^ (n + 1) + 1
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
_private.Mathlib.Combinatorics.SimpleGraph.FiveWheelLike.0.SimpleGraph.IsNClique.insert_insert_erase : ∀ {α : Type u_1} {a b c : α} {s : Finset α} {G : SimpleGraph α} {r : ℕ} [inst : DecidableEq α],
  G.IsNClique r (insert a s) →
    c ∈ s → a ∉ s → (∀ w ∈ insert a s, w ≠ c → G.Adj w b) → G.IsNClique r (insert a (insert b (s.erase c)))
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
UpperHalfPlane.instMeasurableSpace : MeasurableSpace UpperHalfPlane
-- Mathlib.Data.NNReal.Defs
Set.OrdConnected.preimage_real_toNNReal : ∀ {t : Set NNReal}, t.OrdConnected → (Real.toNNReal ⁻¹' t).OrdConnected
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.sInf_adj : ∀ {V : Type u_2} {a b : V} {s : Set (Digraph V)}, (sInf s).Adj a b ↔ ∀ G ∈ s, G.Adj a b
-- Mathlib.MeasureTheory.Function.AEEqOfLIntegral
MeasureTheory.AEMeasurable.ae_eq_of_forall_setLIntegral_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g μ →
      ∫⁻ (x : α), f x ∂μ ≠ ⊤ →
        ∫⁻ (x : α), g x ∂μ ≠ ⊤ →
          (∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ) → f =ᵐ[μ] g
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.SMulCandidate.h : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} {α : R₀ ⟶ R.obj}
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} {φ : M₀.presheaf ⟶ A.obj} {X : Cᵒᵖ}
  {r : ↑(R.obj.obj X)} {m : ↑(A.obj.obj X)} (self : PresheafOfModules.Sheafify.SMulCandidate α φ r m) ⦃Y : Cᵒᵖ⦄
  (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
  (CategoryTheory.ConcreteCategory.hom (α.app Y)) r₀ = (CategoryTheory.ConcreteCategory.hom (R.obj.map f)) r →
    ∀ (m₀ : ↑(M₀.obj Y)),
      (CategoryTheory.ConcreteCategory.hom (φ.app Y)) m₀ = (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) m →
        (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) self.x =
          (CategoryTheory.ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.leadingCoeff_derivative : ∀ {R : Type u} [inst : Semiring R] [IsAddTorsionFree R] (p : Polynomial R),
  (Polynomial.derivative p).leadingCoeff = p.leadingCoeff * ↑p.natDegree
-- Init.Data.Int.Order
Int.add_pos_of_pos_of_nonneg : ∀ {a b : ℤ}, 0 < a → 0 ≤ b → 0 < a + b
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_strictMono : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K], StrictMono NNRat.cast
-- Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {ε : ℝ},
  Continuous f →
    0 < ε →
      ∃ g, ContDiff ℝ (↑⊤) g ∧ ∀ (a : E) (δ : ℝ), (∀ x ∈ Metric.ball a ε, dist (f x) (f a) ≤ δ) → dist (g a) (f a) ≤ δ
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.valuation_p_pow_mul : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) (c : ℤ_[p]), c ≠ 0 → (↑p ^ n * c).valuation = n + c.valuation
-- Mathlib.Computability.StateTransition
StateTransition.eval_maximal₁ : ∀ {σ : Type u_1} {f : σ → Option σ} {a b : σ}, b ∈ StateTransition.eval f a → ∀ (c : σ), ¬StateTransition.Reaches₁ f b c
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMul : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R],
  CanLift (Set R) (NonUnitalSubsemiring R) SetLike.coe fun s =>
    0 ∈ s ∧ (∀ {x y : R}, x ∈ s → y ∈ s → x + y ∈ s) ∧ ∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidt_zero : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (n : ι),
  InnerProductSpace.gramSchmidt 𝕜 0 n = 0
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- An equalizer diagram gives rise to a regular monomorphism.  -/
CategoryTheory.Fork.IsLimit.regularMono : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : C} →
      {p₁ p₂ : A ⟶ B} →
        {c : CategoryTheory.Limits.Fork p₁ p₂} → CategoryTheory.Limits.IsLimit c → CategoryTheory.RegularMono c.ι
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.relIso_enum' : ∀ {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s] (f : r ≃r s)
  (o : Ordinal.{u}) (hr : o < Ordinal.type r) (hs : o < Ordinal.type s),
  f ((Ordinal.enum r) ⟨o, hr⟩) = (Ordinal.enum s) ⟨o, hs⟩
-- Init.System.IO
/-- Converts an `EIO ε` action that might throw an exception of type `ε` into an exception-free `BaseIO`
action that returns an `Except` value.
 -/
EIO.toBaseIO : {ε α : Type} → EIO ε α → BaseIO (Except ε α)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.algebraMap_injective : ∀ (K : Type u) [inst : CommRing K] [inst_1 : IsDomain K], Function.Injective ⇑(algebraMap (Polynomial K) (RatFunc K))
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.toCommRing : {α : Type u_1} → [BooleanRing α] → CommRing α
-- Init.Data.String.Basic
String.get'_eq : ∀ (s : String) (p : String.Pos.Raw) (h : ¬String.Pos.Raw.atEnd s p = true),
  String.Pos.Raw.get' s p h = String.Pos.Raw.get s p