mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.iso_image_comp_eq_map_iff_eq_comp : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {v : V} {C : G.ConnectedComponent},
  G'.connectedComponentMk (φ v) = SimpleGraph.ConnectedComponent.map (RelIso.toRelEmbedding φ).toRelHom C ↔
    G.connectedComponentMk v = C
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁.union m₂},
  Std.DHashMap.Const.get (m₁.union m₂) k h' = Std.DHashMap.Const.get m₁ k ⋯
-- Std.Http.Data.URI.Parser
/-- Parses an HTTP `Host` header value.
 -/
Std.Http.URI.Parser.parseHostHeader : optParam Std.Http.URI.Config { } → Std.Internal.Parsec.ByteArray.Parser (Std.Http.URI.Host × Std.Http.URI.Port)
-- Mathlib.FieldTheory.PrimeField
/-- The smallest subfield of a field of characteristic `0` is (the image of) `ℚ`.
 -/
Subfield.bot_eq_of_charZero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : CharZero K], ⊥ = (algebraMap ℚ K).fieldRange
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- Any compact set in a pseudometric space can be covered by finitely many balls of a given
positive radius  -/
finite_cover_balls_of_compact : ∀ {X : Type u_2} [inst : PseudoMetricSpace X] {s : Set X},
  IsCompact s → ∀ {e : ℝ}, 0 < e → ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, Metric.ball x e
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_inv_pointwise_smul_iff : ∀ {K : Type u} [inst : Field K] {G : Type u_1} [inst_1 : Group G] [inst_2 : MulSemiringAction G K] {g : G}
  {S : ValuationSubring K} {x : K}, x ∈ g⁻¹ • S ↔ g • x ∈ S
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.nsmul_eq_sum_const : ∀ {M : Type u_4} [inst : AddCommMonoid M] (b : M) (n : ℕ), n • b = ∑ _k ∈ Finset.range n, b
-- Lean.Data.KVMap
Lean.KVMap.getString : Lean.KVMap → Lean.Name → optParam String "" → String
-- Mathlib.Data.List.Sublists
_private.Mathlib.Data.List.Sublists.0.List.sublistsLenAux.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : ℕ → List α → (List α → β) → List β → Sort u_3) (x : List α) (f : List α → β)
  (r : List β) (h_1 : (x : List α) → (f : List α → β) → (r : List β) → motive 0 x f r)
  (h_2 : (n : ℕ) → (x : List α → β) → (r : List β) → motive n.succ [] x r)
  (h_3 : (n : ℕ) → (a : α) → (l : List α) → (f : List α → β) → (r : List β) → motive n.succ (a :: l) f r),
  (match 0, x, f, r with
    | 0, x, f, r => h_1 x f r
    | n.succ, [], x, r => h_2 n x r
    | n.succ, a :: l, f, r => h_3 n a l f r) =
    h_1 x f r
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {km : α}, t.maxKey? = some km → t.getKey! km = km
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.struct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preregular C] →
      [inst_2 : CategoryTheory.FinitaryExtensive C] →
        CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v)) → Type (max u v)
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- A copy of `WithLp.volume_preserving_symm_measurableEquiv_toLp_prod`
for the canonical spelling of the equivalence.  -/
WithLp.volume_preserving_ofLp : ∀ (U : Type u_4) (V : Type u_5) [inst : NormedAddCommGroup U] [inst_1 : InnerProductSpace ℝ U]
  [inst_2 : MeasurableSpace U] [inst_3 : BorelSpace U] [inst_4 : FiniteDimensional ℝ U] [inst_5 : NormedAddCommGroup V]
  [inst_6 : InnerProductSpace ℝ V] [inst_7 : MeasurableSpace V] [inst_8 : BorelSpace V]
  [inst_9 : FiniteDimensional ℝ V],
  MeasureTheory.MeasurePreserving WithLp.ofLp MeasureTheory.volume MeasureTheory.volume
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr : Lean.ToJson Lean.Lsp.RefIdent.RefIdentJsonRepr
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup_P : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular] {ι : Type u_1}
  (D : ι → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ) (hι : HasCardinalLT ι κ) (a : J),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup D hι).P a = (⨆ i, (D i).P) a
-- Mathlib.Algebra.BigOperators.Finprod
/-- A set `s` is nonempty if the product of some function over `s` is not equal to `1`.  -/
nonempty_of_finprod_mem_ne_one : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set α},
  ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1 → s.Nonempty
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
ChainComplex.mkHom.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (P Q : ChainComplex V ℕ) (zero zero_1 : P.X 0 ⟶ Q.X 0) (e_zero : zero = zero_1) (one one_1 : P.X 1 ⟶ Q.X 1)
  (e_one : one = one_1)
  (one_zero_comm : CategoryTheory.CategoryStruct.comp one (Q.d 1 0) = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero)
  (succ succ_1 :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X n) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
              CategoryTheory.CategoryStruct.comp f' (Q.d (n + 1) n) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
          CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 2) (n + 1)) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst),
  succ = succ_1 → P.mkHom Q zero one one_zero_comm succ = P.mkHom Q zero_1 one_1 ⋯ succ_1
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.smul_def : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {X : Type u_4}
  [inst_3 : SMul L X] {F : IntermediateField K L} (g : ↥F) (m : X), g • m = ↑g • m
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N →ₗ[R] P), LinearMap.lTensor M f = TensorProduct.map LinearMap.id f
-- Init.Control.Basic
/-- Lifts a monadic action that returns a state and a value in the inner monad to an action in the
outer monad. The extra state information is used to restore the results of effects from the
reverse lift passed to `liftWith`'s parameter.
 -/
MonadControl.restoreM : {m : semiOutParam (Type u → Type v)} →
  {n : Type u → Type w} → [self : MonadControl m n] → {α : Type u} → m (MonadControl.stM m n α) → n α
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.addLeftMono : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddZeroClass α] [AddLeftMono α],
  (∀ (a : α), 0 ≤ a) → AddLeftMono (WithZero α)
-- Mathlib.Analysis.Analytic.IsolatedZeros
AnalyticAt.frequently_zero_iff_eventually_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {w : 𝕜},
  AnalyticAt 𝕜 f w → ((∃ᶠ (z : 𝕜) in nhdsWithin w {w}ᶜ, f z = 0) ↔ ∀ᶠ (z : 𝕜) in nhds w, f z = 0)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.mul_integral_upcrossingsBefore_le_integral_pos_part_aux : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ}
  {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    a < b →
      (b - a) * ∫ (x : Ω), ↑(MeasureTheory.upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun_congr : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ι → Type u_10}
  {m : (x : ι) → MeasurableSpace (β x)} {f : (x : ι) → Ω → β x},
  ⇑κ =ᵐ[μ] ⇑η → (ProbabilityTheory.Kernel.iIndepFun f κ μ ↔ ProbabilityTheory.Kernel.iIndepFun f η μ)
-- Mathlib.Topology.VectorBundle.Constructions
/-- The product of two vector bundles is a vector bundle.  -/
VectorBundle.prod : ∀ (𝕜 : Type u_1) {B : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : TopologicalSpace B] (F₁ : Type u_3)
  [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] (E₁ : B → Type u_4)
  [inst_4 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] (F₂ : Type u_5) [inst_5 : NormedAddCommGroup F₂]
  [inst_6 : NormedSpace 𝕜 F₂] (E₂ : B → Type u_6) [inst_7 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_8 : (x : B) → AddCommMonoid (E₁ x)] [inst_9 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_10 : (x : B) → AddCommMonoid (E₂ x)] [inst_11 : (x : B) → Module 𝕜 (E₂ x)]
  [inst_12 : (x : B) → TopologicalSpace (E₁ x)] [inst_13 : (x : B) → TopologicalSpace (E₂ x)]
  [inst_14 : FiberBundle F₁ E₁] [inst_15 : FiberBundle F₂ E₂] [VectorBundle 𝕜 F₁ E₁] [VectorBundle 𝕜 F₂ E₂],
  VectorBundle 𝕜 (F₁ × F₂) fun x => E₁ x × E₂ x
-- Mathlib.Topology.Germ
Filter.Germ.value_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (c : Y) (x : X), (↑c).value = c
-- Init.Notation
Lean.Parser.Category.mk : Lean.Parser.Category
-- Mathlib.Data.Seq.Computation
Stream'.cons.eq_1 : ∀ {α : Type u} (a : α) (s : Stream' α), Stream'.cons a s 0 = a
-- Mathlib.RingTheory.LocalRing.LocalSubring
instIsLocalRingSubtypeMemSubringMapOfNontrivial : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [Nontrivial S] (f : R →+* S) (s : Subring R)
  [IsLocalRing ↥s], IsLocalRing ↥(Subring.map f s)
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
/-- If `I` is an ideal in a `ℚ`-algebra `A`, then the divided power structure on `I` given by
`dpow n x = x ^ n / n!` is the only possible one.  -/
DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul : ∀ {R : Type u_1} [inst : CommSemiring R] (I : Ideal R) [inst_1 : Algebra ℚ R] (hI : DividedPowers I) {n : ℕ} {x : R},
  x ∈ I → hI.dpow n x = Ring.inverse ↑n.factorial • x ^ n
-- Mathlib.AlgebraicGeometry.Morphisms.IsIso
AlgebraicGeometry.isomorphisms_eq_stalkwise : CategoryTheory.MorphismProperty.isomorphisms AlgebraicGeometry.Scheme =
  (CategoryTheory.MorphismProperty.isomorphisms TopCat).inverseImage AlgebraicGeometry.Scheme.forgetToTop ⊓
    AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f
-- Mathlib.Data.Nat.ModEq
/-- Cancel left multiplication on both sides of the `≡` and in the modulus.

For cancelling left multiplication in the modulus, see `Nat.ModEq.of_mul_left`.  -/
Nat.ModEq.mul_left_cancel' : ∀ {a b c m : ℕ}, c ≠ 0 → c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m]
-- Std.Http.Data.Version
Std.Http.Version.instToString : ToString Std.Http.Version
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.instSemilatticeSup : SemilatticeSup ℚ
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.toEquiv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_5} →
                  [inst_5 : TopologicalSpace H] →
                    {H' : Type u_6} →
                      [inst_6 : TopologicalSpace H'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {M : Type u_9} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {M' : Type u_10} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        {n : WithTop ℕ∞} → Diffeomorph I I' M M' n → M ≃ M'
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.ofMon.eq_1 : ∀ (m : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Poly.ofMon m = Lean.Grind.CommRing.Poly.add 1 m (Lean.Grind.CommRing.Poly.num 0)
-- Mathlib.NumberTheory.Modular
/-- Second Fundamental Domain Lemma: if `z ∈ 𝒟ᵒ` and `g • z ∈ 𝒟`, then `g = ± 1`.  -/
ModularGroup.eq_one_or_neg_one_of_mem_fdo_mem_fd : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane},
  z ∈ ModularGroup.fdo → g • z ∈ ModularGroup.fd → g = 1 ∨ g = -1
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.branch.sizeOf_spec : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : SizeOf Γ] [inst_1 : SizeOf Λ] [inst_2 : SizeOf σ]
  (a : Γ → σ → Bool) (a_1 a_2 : Turing.TM1.Stmt Γ Λ σ),
  sizeOf (Turing.TM1.Stmt.branch a a_1 a_2) = 1 + sizeOf a_1 + sizeOf a_2
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingSeminorm.mk : {R : Type u_2} →
  [inst : NonAssocRing R] →
    (toAddGroupSeminorm : AddGroupSeminorm R) →
      toAddGroupSeminorm.toFun 1 = 1 →
        (∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y) →
          MulRingSeminorm R
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → (Std.DHashMap.Raw.Const.toArray m).isEmpty = m.isEmpty
-- Init.Conv
/-- `ext x` traverses into a binder (a `fun x => e` or `∀ x, e` expression)
to target `e`, introducing name `x` in the process.  -/
Lean.Parser.Tactic.Conv.ext : Lean.ParserDescr
-- Std.Internal.UV.System
Std.Internal.UV.System.instInhabitedUnameInfo.default : Std.Internal.UV.System.UnameInfo
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentEdit.mk : Lean.Lsp.VersionedTextDocumentIdentifier → Lean.Lsp.TextEditBatch → Lean.Lsp.TextDocumentEdit
-- Mathlib.Algebra.Homology.ImageToKernel
imageToKernel'.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) (g : B ⟶ C) [inst_2 : CategoryTheory.Limits.HasKernels V] [inst_3 : CategoryTheory.Limits.HasImages V]
  (w : CategoryTheory.CategoryStruct.comp f g = 0),
  imageToKernel' f g w = CategoryTheory.Limits.kernel.lift g (CategoryTheory.Limits.image.ι f) ⋯
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.comp_fst_iff : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite μ]
  [MeasureTheory.IsFiniteMeasure ν] {f : α → E},
  ν ≠ 0 → (MeasureTheory.Integrable (fun x => f x.1) (μ.prod ν) ↔ MeasureTheory.Integrable f μ)
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.bot_rel_eq_leftRel : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), ⇑(DoubleCoset.setoid ↑⊥ ↑H) = ⇑(QuotientGroup.leftRel H)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.finite_range' : ∀ {α : Type u} [inst : MeasurableSpace α] {β : Type v} (self : MeasureTheory.SimpleFunc α β),
  (Set.range self.toFun).Finite
-- Mathlib.Data.Rat.Cast.Defs
MonoidWithZeroHomClass.ext_nnrat_iff : ∀ {M₀ : Type u_5} [inst : MonoidWithZero M₀] {f g : ℚ≥0 →*₀ M₀},
  f = g ↔
    f.comp (MonoidWithZeroHom.ofClass (Nat.castRingHom ℚ≥0)) = g.comp (MonoidWithZeroHom.ofClass (Nat.castRingHom ℚ≥0))
-- Mathlib.Algebra.Order.Group.Lattice
sup_mul : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulRightMono α] (a b c : α), (a ⊔ b) * c = a * c ⊔ b * c
-- Mathlib.Algebra.Lie.Abelian
/-- A Lie (ring) module is trivial iff all brackets vanish.  -/
LieModule.IsTrivial : (L : Type v) → (M : Type w) → [Bracket L M] → [Zero M] → Prop
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.ofIsoColimit_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit r)
  (i : r ≅ t) (s : CategoryTheory.Limits.Cocone F),
  (P.ofIsoColimit i).desc s = CategoryTheory.CategoryStruct.comp i.inv.hom (P.desc s)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_eq_find : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {k : α} {l : List ((a : α) × β a)},
  Std.Internal.List.getEntry? k l = List.find? (fun x => x.fst == k) l
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.falsum : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ}, FirstOrder.Language.BoundedFormula.falsum.IsQF
-- Lean.Data.Options
/-- A strongly-typed reference to an option.  -/
Lean.Option : Type → Type
-- Mathlib.Algebra.Polynomial.Smeval
/-- Evaluate a polynomial `p` in the scalar semiring `R` at an element `x` in the target `S` using
scalar multiple `R`-action.  -/
Polynomial.smeval : {R : Type u_3} →
  [inst : Semiring R] →
    Polynomial R → {S : Type u_4} → [inst_1 : AddCommMonoid S] → [Pow S ℕ] → [MulActionWithZero R S] → S → S
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findSomeM?.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.Decl.relabel_atom : ∀ {α β : Type} {idx : ℕ} {a : β} {decls : Array (Std.Sat.AIG.Decl α)} {r : α → β} {hidx : idx < decls.size},
  Std.Sat.AIG.Decl.relabel r decls[idx] = Std.Sat.AIG.Decl.atom a → ∃ x, decls[idx] = Std.Sat.AIG.Decl.atom x ∧ a = r x
-- Mathlib.Probability.Kernel.Representation
MeasureTheory.Measure.exists_measurable_map_eq : ∀ {Y : Type u_2} [Nonempty Y] {mY : MeasurableSpace Y} [StandardBorelSpace Y] (μ : MeasureTheory.Measure Y)
  [MeasureTheory.IsProbabilityMeasure μ], ∃ f, Measurable f ∧ MeasureTheory.Measure.map f MeasureTheory.volume = μ
-- Mathlib.RingTheory.PowerBasis
PowerBasis.equivOfRoot_map : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] {S' : Type u_7} [inst_2 : CommRing S']
  [inst_3 : Algebra A S] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S')
  (h₁ : (Polynomial.aeval pb.gen) (minpoly A (pb.map e).gen) = 0)
  (h₂ : (Polynomial.aeval (pb.map e).gen) (minpoly A pb.gen) = 0), pb.equivOfRoot (pb.map e) h₁ h₂ = e
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Monoidal.μ_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
      (F.map (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)) =
    CategoryTheory.SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj Y)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.left_invariance' : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ {s : Set H} {x : H} {f : H → H'} {e' : OpenPartialHomeomorph H' H'},
      e' ∈ G' → s ⊆ f ⁻¹' e'.source → f x ∈ e'.source → P f s x → P (↑e' ∘ f) s x
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.revMatchAt?_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {endPos : s.Pos},
  String.Slice.Pattern.Model.revMatchAt? pat endPos = none ↔ ¬String.Slice.Pattern.Model.RevMatchesAt pat endPos
-- Mathlib.CategoryTheory.Sites.Coherent.Basic
CategoryTheory.Preregular.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  (∀ {X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ Y) [CategoryTheory.EffectiveEpi g],
      ∃ W h,
        ∃ (_ : CategoryTheory.EffectiveEpi h),
          ∃ i, CategoryTheory.CategoryStruct.comp i g = CategoryTheory.CategoryStruct.comp h f) →
    CategoryTheory.Preregular C
-- Mathlib.Topology.Category.Locale
CompHausToLocale.faithful : (compHausToTop.comp topToLocale).Faithful
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] {M N : CategoryTheory.AddMod D A} (f₁ f₂ : M ⟶ N),
  f₁.hom = f₂.hom → f₁ = f₂
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.mul_le_iff_le_one_right : ∀ {α : Type u_1} [inst : LE α] [inst_1 : MulOneClass α] [MulLeftMono α] {a b : α},
  MulLECancellable a → (a * b ≤ a ↔ b ≤ 1)
-- Mathlib.Order.Filter.CardinalInter
Filter.cardinalInter_ofCardinalUnion : ∀ {α : Type u} {c : Cardinal.{u}} (l : Set (Set α)) (hc : 2 < c)
  (h₁ : ∀ (S : Set (Set α)), Cardinal.mk ↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l) (h₂ : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l),
  CardinalInterFilter (Filter.ofCardinalUnion l hc h₁ h₂) c
-- Lean.Data.Name
Lean.Name.updatePrefix : Lean.Name → Lean.Name → Lean.Name
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.prod_symm : ∀ {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace X'] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Y']
  (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y'), (eX.prod eY).symm = eX.symm.prod eY.symm
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.instHasFactorizationOfHasFunctorialFactorization : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C)
  [W₁.HasFunctorialFactorization W₂], W₁.HasFactorization W₂
-- Mathlib.Topology.Compactness.SigmaCompact
compactCovering.congr_simp : ∀ (X : Type u_1) [inst : TopologicalSpace X] [inst_1 : SigmaCompactSpace X] (a a_1 : ℕ),
  a = a_1 → ∀ (a_2 a_3 : X), a_2 = a_3 → compactCovering X a a_2 = compactCovering X a_1 a_3
-- Mathlib.Algebra.Group.Center
Set.center_subset_centralizer : ∀ {M : Type u_1} [inst : Mul M] (S : Set M), Set.center M ⊆ S.centralizer
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.comp_continuous_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) {α : Type u_11} [inst_6 : TopologicalSpace α] {g : α → E},
  Continuous (⇑f ∘ g) ↔ Continuous g
-- Mathlib.Topology.Algebra.Group.Torsor
IsTopologicalAddTorsor.mk : ∀ {V : Type u_1} [inst : AddGroup V] [inst_1 : TopologicalSpace V] {P : Type u_2} [inst_2 : AddTorsor V P]
  [inst_3 : TopologicalSpace P] [toContinuousVAdd : ContinuousVAdd V P],
  (Continuous fun x => x.1 -ᵥ x.2) → IsTopologicalAddTorsor P
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instNonUnitalCommSemiringOfIsTopologicalSemiring : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalCommSemiring β] →
          [IsTopologicalSemiring β] → NonUnitalCommSemiring (CompactlySupportedContinuousMap α β)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_indicator₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {s t : Set α},
  MeasureTheory.NullMeasurableSet s (μ.restrict t) → ∫⁻ (a : α) in t, s.indicator f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ