mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMon_map_hom : ∀ {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 D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] {X Y : CategoryTheory.Mon C} (f : X ⟶ Y),
  (F.mapMon.map f).hom = F.map f.hom
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false → (Std.DTreeMap.Const.ofList l cmp).getKeyD k fallback = fallback
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.single_neg : ∀ {k : Type u_1} {G : Type u_2} [inst : AddGroup k] (a : G) (b : k),
  SkewMonoidAlgebra.single a (-b) = -SkewMonoidAlgebra.single a b
-- Lean.Elab.PreDefinition.Structural.Main
_private.Lean.Elab.PreDefinition.Structural.Main.0.Lean.Elab.Structural.elimMutualRecursion : Array Lean.Elab.PreDefinition →
  Lean.Elab.FixedParamPerms →
    Array Lean.Expr → Array Lean.Elab.Structural.RecArgInfo → Lean.MetaM (Array Lean.Elab.PreDefinition)
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_eq_ofReal_norm_sq_right_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {v w : E}, inner 𝕜 v w = ↑‖w‖ ^ 2 ↔ inner 𝕜 (v - w) w = 0
-- Lean.Parser.Term
Lean.Parser.Term.match.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.mem_inv_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {A : Type u_4} [inst : GroupWithZero G₀] [inst_1 : AddGroup A] [inst_2 : DistribMulAction G₀ A]
  {a : G₀}, a ≠ 0 → ∀ (S : AddSubgroup A) (x : A), x ∈ a⁻¹ • S ↔ a • x ∈ S
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinAt.add : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {pf pg : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E},
  HasFPowerSeriesWithinAt f pf s x → HasFPowerSeriesWithinAt g pg s x → HasFPowerSeriesWithinAt (f + g) (pf + pg) s x
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.coe_id : ∀ (α : Type u_2) [inst : InfSet α], ⇑(sInfHom.id α) = id
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.fullyFaithfulForget_preimage_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) {X Y : SheafOfModules R}
  (φ : (SheafOfModules.forget R).obj X ⟶ (SheafOfModules.forget R).obj Y),
  ((SheafOfModules.fullyFaithfulForget R).preimage φ).val = φ
-- Mathlib.Logic.Function.Basic
Function.instIsStrictWeakOrderSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [IsStrictWeakOrder α r], IsStrictWeakOrder α (Function.swap r)
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.instInhabited : {α : Type u_1} → [inst : HeytingAlgebra α] → Inhabited (Heyting.Regular α)
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_natCast_lt_one_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ}, ‖↑n‖ < 1 ↔ p ∣ n
-- Mathlib.RingTheory.SurjectiveOnStalks
_private.Mathlib.RingTheory.SurjectiveOnStalks.0.RingHom.SurjectiveOnStalks.tensorProductMap_id : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {T : Type u_3} [inst_2 : CommRing T]
  {S' : Type u_4} [inst_3 : CommRing S'] [inst_4 : Algebra R S] [inst_5 : Algebra R T] [inst_6 : Algebra R S']
  {f : S →ₐ[R] S'}, f.SurjectiveOnStalks → (Algebra.TensorProduct.map f (AlgHom.id R T)).SurjectiveOnStalks
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Submodule.cardQuot_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submodule R M),
  S.cardQuot = Nat.card (M ⧸ S)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.insert_eq_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {p : α × β},
  insert p t = t.insert p.1 p.2
-- Lean.Elab.DocString
/-- Built-in code block suggestions, for bootstrapping
 -/
Lean.Doc.builtinCodeBlockSuggestions : IO.Ref (Array (Lean.Name × Lean.Doc.CodeBlockSuggester))
-- Mathlib.Order.InitialSeg
/-- A relation isomorphism is an initial segment embedding  -/
RelIso.toInitialSeg : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ≃r s → InitialSeg r s
-- Mathlib.Order.Monotone.Monovary
AntivaryOn.comp_antitone_on_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} {s : Set ι},
  AntivaryOn f g s → Antitone f' → MonovaryOn (f' ∘ f) g s
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of a constant function is `⊤` if the constant is zero and `0` otherwise.
 -/
meromorphicOrderAt_const_natCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] (z₀ : 𝕜) (n : ℕ) [inst_3 : Decidable (↑n = 0)],
  meromorphicOrderAt (↑n) z₀ = if ↑n = 0 then ⊤ else 0
-- Mathlib.Data.Set.Lattice
Set.iUnion_sumElim : ∀ {α : Type u_1} {ι : Type u_12} {σ : Type u_13} (s : ι → Set α) (t : σ → Set α),
  ⋃ x, Sum.elim s t x = (⋃ x, s x) ∪ ⋃ x, t x
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_eq : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f g : α → β}, ↑f = ↑g ↔ f =ᶠ[l] g
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
/-- The integral of `ω` along `[a -[ℝ] b]`, as a function of `b`, has derivative `ω a` at `b = a`.
This is a `HasFDerivWithinAt` version assuming that `ω` is continuous on `s`.  -/
HasFDerivWithinAt.curveIntegral_segment_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F]
  [CompleteSpace F] {a : E} {s : Set E} {ω : E → E →L[𝕜] F},
  Convex ℝ s → ContinuousOn ω s → a ∈ s → HasFDerivWithinAt (fun x => ∫ᶜ (x : E) in Path.segment a x, ω x) (ω a) s a
-- Mathlib.Geometry.Manifold.Notation
/-- Delaborator for `UniqueMDiffWithinAt` using the custom elaborator.  -/
Manifold.delabUniqueMDiffWithinAt : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.Integrable.integral_norm_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} ⦃f : γ → E⦄,
  MeasureTheory.Integrable f ((η.comp κ) a) → MeasureTheory.Integrable (fun x => ∫ (y : γ), ‖f y‖ ∂η x) (κ a)
-- Lean.Compiler.IR.CompilerM
Lean.IR.LogEntry.step.sizeOf_spec : ∀ (cls : Lean.Name) (decls : Array Lean.IR.Decl),
  sizeOf (Lean.IR.LogEntry.step cls decls) = 1 + sizeOf cls + sizeOf decls
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.mk.inj : ∀ {G : Type u_1} {H : Type u_2} {inst : Add G} {inst_1 : Add H} {a : G} {b : H} {toEquiv : G ≃ H}
  {map_add_const' : ∀ (x : G), toEquiv.toFun (x + a) = toEquiv.toFun x + b} {toEquiv_1 : G ≃ H}
  {map_add_const'_1 : ∀ (x : G), toEquiv_1.toFun (x + a) = toEquiv_1.toFun x + b},
  { toEquiv := toEquiv, map_add_const' := map_add_const' } =
      { toEquiv := toEquiv_1, map_add_const' := map_add_const'_1 } →
    toEquiv = toEquiv_1
-- Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer
Matrix.SpecialLinearGroup.lineStab_fix_of_span : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (v : ι → F),
  v ≠ 0 → ∀ A ∈ Matrix.SpecialLinearGroup.lineStab (F ∙ v), A • v = v
-- Mathlib.Algebra.Lie.Extension
/-- Given an extension of `L` by `M` whose kernel `M` is abelian, the kernel `M` gets an `R`-linear
`L`-module structure. We do not make this an instance, because we may have to work with more than
one extension.  -/
LieAlgebra.Extension.lieModuleOf : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] [inst_5 : IsLieAbelian M] (E : LieAlgebra.Extension R M L),
  LieModule R L M
-- Mathlib.AlgebraicGeometry.PointsPi
AlgebraicGeometry.pointsPi_surjective : ∀ {ι : Type u} (R : ι → CommRingCat) (X : AlgebraicGeometry.Scheme) [CompactSpace ↥X] [∀ (i : ι), IsLocalRing ↑(R i)],
  Function.Surjective (AlgebraicGeometry.pointsPi R X)
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.linearMap_eq_zero_iff_of_span_eq_top : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_8}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₗ[R] N) {S : Set M},
  Submodule.span R S = ⊤ → (f = 0 ↔ ∀ (s : ↑S), f ↑s = 0)
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.map_id_lsmul_eq_lsmul_algebraMap : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {f : M →ₗ[R] N} (hf : IsBaseChange S f) (x : R),
  IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M) x) = ↑R ((LinearMap.lsmul S N) ((algebraMap R S) x))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α}
  (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ Std.ExtDTreeMap.Const.insertMany t l},
  Std.ExtDTreeMap.Const.get (Std.ExtDTreeMap.Const.insertMany t l) k h' = Std.ExtDTreeMap.Const.get t k ⋯
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
/-- Auxiliary definition for `desc`.  -/
ComplexShape.Embedding.AreComplementary.desc.aux : {ι : Type u_1} → (X : ι → Type u_5) → (i j : ι) → i = j → X i ≃ X j
-- Aesop.Script.TacticState
Aesop.Script.TacticState.solveVisibleGoals : Aesop.Script.TacticState → Aesop.Script.TacticState
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.norm_zero_iff : ∀ (A : Type u_1) {E : Type u_2} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : Norm E] [CStarModule A E] (x : E), ‖x‖ = 0 ↔ x = 0
-- Mathlib.Tactic.Widget.SelectPanelUtils
/-- Cursor position in the file at which the widget is being displayed.  -/
SelectInsertParams.pos : SelectInsertParams → Lean.Lsp.Position
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F}
  (h : E.IsPointwiseLeftKanExtension),
  (CategoryTheory.StructuredArrow.right E).IsLeftKanExtension (CategoryTheory.StructuredArrow.hom E)
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- The trivial group is the normal closure of a finite set of relations.  -/
Subgroup.IsFinitelyNormallyGenerated.bot : ∀ {G : Type u_1} [inst : Group G], ⊥.IsFinitelyNormallyGenerated
-- Mathlib.RingTheory.PolynomialAlgebra
/-- (Implementation detail).
The function underlying `A ⊗[R] R[X] →ₐ[R] A[X]`,
as a linear map.
 -/
PolyEquivTensor.toFunLinear : (R : Type u_1) →
  (A : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → TensorProduct R A (Polynomial R) →ₗ[R] Polynomial A
-- Mathlib.Algebra.Quaternion
/-- `QuaternionAlgebra.imK` as a `LinearMap`  -/
QuaternionAlgebra.imKₗ : {R : Type u_3} → (c₁ c₂ c₃ : R) → [inst : CommRing R] → QuaternionAlgebra R c₁ c₂ c₃ →ₗ[R] R
-- Mathlib.Topology.MetricSpace.GromovHausdorff
NonemptyCompacts.kuratowskiEmbedding.congr_simp : ∀ (α : Type u) [inst : MetricSpace α] [inst_1 : CompactSpace α] [inst_2 : Nonempty α],
  NonemptyCompacts.kuratowskiEmbedding α = NonemptyCompacts.kuratowskiEmbedding α
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
_private.Mathlib.LinearAlgebra.Matrix.FixedDetMatrices.0.FixedDetMatrices.termΔ_ : Lean.ParserDescr
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.subtype_apply : ∀ {R : Type u} {M : Type v} [inst : SMul R M] {p : SubMulAction R M} (x : ↥p), p.subtype x = ↑x
-- Lean.Elab.Tactic.Omega.Core
/-- If we have already solved some equalities, apply those to some new `Fact`.
 -/
Lean.Elab.Tactic.Omega.Problem.replayEliminations : Lean.Elab.Tactic.Omega.Problem → Lean.Elab.Tactic.Omega.Fact → Lean.Elab.Tactic.Omega.Fact
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `DFunLike.coe_injective`. -/
MeasureTheory.VectorMeasure.coe_injective : ∀ {F : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (α → Sort u_3)} [self : DFunLike F α β],
  Function.Injective DFunLike.coe
-- Mathlib.Data.Finsupp.Defs
Finsupp.support_zero : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M], Finsupp.support 0 = ∅
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- The variation of `f` along the image of `{0, …, n}` under a monotone sequence `u` is the sum of
the distances between consecutive values.  -/
eVariationOn.image_range_of_monotone : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {u : ℕ → α},
  Monotone u → ∀ (n : ℕ), eVariationOn f (u '' Set.Iic n) = ∑ i ∈ Finset.range n, edist (f (u i)) (f (u (i + 1)))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.le_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} {N₁ N₂ : M.Submodule}, N₁ ≤ N₂ ↔ ∀ (X : Cᵒᵖ), N₁.obj X ≤ N₂.obj X
-- Mathlib.Computability.Encoding
Computability.sectionΓ'Bool_inclusionBoolΓ' : ∀ {b : Bool}, Computability.sectionΓ'Bool (Computability.inclusionBoolΓ' b) = b
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.coe_ofSeqClosedGraph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_5} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {g : E →ₗ[𝕜] F}
  (hg :
    ∀ (u : ℕ → E) (x : E) (y : F),
      Filter.Tendsto u Filter.atTop (nhds x) → Filter.Tendsto (⇑g ∘ u) Filter.atTop (nhds y) → y = g x),
  ↑(ContinuousLinearMap.ofSeqClosedGraph hg) = g
-- Batteries.Data.Float.Basic
/-- Divide two natural numbers, to produce a correctly rounded (nearest-ties-to-even) `Float` result.
 -/
Nat.divFloat : ℕ → ℕ → Float
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.instHSubOffset_3 : HSub Std.Time.PlainTime Std.Time.Minute.Offset Std.Time.PlainTime
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.find?_some_mem_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBTree.RBSet α cmp}, t.find? x = some y → y ∈ t.toList
-- Mathlib.Topology.Gluing
TopCat.GlueData.preimage_range : ∀ (D : TopCat.GlueData) (i j : D.J),
  ⇑(CategoryTheory.ConcreteCategory.hom (D.ι j)) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) =
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.f j i))
-- Mathlib.MeasureTheory.Measure.MeasureSpace
AEMeasurable.nullMeasurableSet_preimage : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β} {s : Set β}, AEMeasurable f μ → MeasurableSet s → MeasureTheory.NullMeasurableSet (f ⁻¹' s) μ
-- Mathlib.LinearAlgebra.Finsupp.Pi
Equiv.funUnique.eq_1 : ∀ (α : Sort u) (β : Sort u_1) [inst : Unique α], Equiv.funUnique α β = Equiv.piUnique fun a => β
-- Mathlib.Analysis.Calculus.MeanValue
Convex.instPathConnectedSpace : ∀ {𝕜 : Type u_3} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜], PathConnectedSpace 𝕜
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_iInf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) {ι : Type u_3} (P : ι → CategoryTheory.MorphismProperty D),
  (⨅ i, P i).inverseImage F = ⨅ i, (P i).inverseImage F
-- Aesop.Util.UnorderedArraySet
/-- O(n)  -/
Aesop.UnorderedArraySet.insert : {α : Type u_1} → [inst : BEq α] → α → Aesop.UnorderedArraySet α → Aesop.UnorderedArraySet α
-- Init.Data.Repr
Nat.toDigitsCore : ℕ → ℕ → ℕ → List Char → List Char
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.ext_iff₂ : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P}
  {f g : M →* N →* P}, f = g ↔ ∀ (x_3 : M) (y : N), (f x_3) y = (g x_3) y
-- Std.Data.ExtDTreeMap.Basic
/-- Partitions a tree map into two tree maps based on a predicate.  -/
Std.ExtDTreeMap.partition : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] →
        ((a : α) → β a → Bool) → Std.ExtDTreeMap α β cmp → Std.ExtDTreeMap α β cmp × Std.ExtDTreeMap α β cmp
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right : ∀ {X Y S T : AlgebraicGeometry.Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T}
  (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens}
  (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US)
  {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT)
  [AlgebraicGeometry.Flat f],
  AlgebraicGeometry.IsAffineOpen US →
    AlgebraicGeometry.IsAffineOpen UT →
      IsCompact ↑UX → IsQuasiSeparated ↑UX → CategoryTheory.IsIso (AlgebraicGeometry.pushoutSection H hUST hUSX hUY)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.uliftCoyonedaCoreprXIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type (max v v₁)))
  [inst_1 : F.IsCorepresentable] (X : C) (f : ULift.{v, v₁} (F.coreprX ⟶ X)),
  (CategoryTheory.ConcreteCategory.hom (F.uliftCoyonedaCoreprXIso.hom.app X)) f =
    (CategoryTheory.ConcreteCategory.hom (F.map f.down)) F.coreprx
-- Mathlib.Geometry.Manifold.SmoothEmbedding
Manifold.IsSmoothEmbedding.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} {E₃ : Type u_4} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : NormedAddCommGroup E₃] [inst_4 : NormedSpace 𝕜 E₃] {H : Type u_6} {G : Type u_8}
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E₁ H}
  {J : ModelWithCorners 𝕜 E₃ G} {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsImmersion I J n f → Topology.IsEmbedding f → Manifold.IsSmoothEmbedding I J n f
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.listL.eq_2 : ∀ {α : Type u_1} (c : RBTree.RBColor) (parent : RBTree.RBNode.Path α) (v : α) (r : RBTree.RBNode α),
  (RBTree.RBNode.Path.left c parent v r).listL = parent.listL
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_series_of_subsingleton : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] {c : ℕ → 𝕜} [Subsingleton E], FormalMultilinearSeries.ofScalars E c = 0
-- Mathlib.RingTheory.Flat.Basic
Algebra.TensorProduct.includeRight_injective : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [Module.Flat R B],
  Function.Injective ⇑(algebraMap R A) → Function.Injective ⇑Algebra.TensorProduct.includeRight
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_add_const_Ico : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x + a) ⁻¹' Set.Ico b c = Set.Ico (b - a) (c - a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constAlter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {f : Option β → Option β},
          (Std.DTreeMap.Internal.Impl.Const.alter! k f t₁).Equiv (Std.DTreeMap.Internal.Impl.Const.alter! k f t₂)
-- Mathlib.Data.NNReal.Defs
Real.one_lt_toNNReal : ∀ {r : ℝ}, 1 < r.toNNReal ↔ 1 < r
-- Mathlib.Data.Fin.Tuple.Curry
Function.FromTypes.curryEquiv_symm_apply : ∀ {n : ℕ} {τ : Type u} (p : Fin n → Type u) (f : Function.FromTypes p τ) (a : (i : Fin n) → p i),
  (Function.FromTypes.curryEquiv p).symm f a = f.uncurry a
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.instInhabitedExtTheorem : Inhabited Lean.Meta.Ext.ExtTheorem
-- Init.Data.Random
/-- Splits a `StdGen` into two separate states.
 -/
stdSplit : StdGen → StdGen × StdGen
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_mem_smul_iff : ∀ {R : Type u} [inst : CommSemiring R] {S : Type u_1} [inst_1 : Ring S] [inst_2 : Algebra R S] {x : S}
  {p : Submodule R S} {y : S}, x ∈ nonZeroDivisors S → (x * y ∈ x • p ↔ y ∈ p)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {w : ℕ} → (n : ℕ) → aig.RefVec w → (curr : ℕ) → curr ≤ n → aig.RefVec (w * curr) → aig.RefVec (w * n)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_insertEntry_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.getValueCast? k (Std.Internal.List.insertEntry k v l) = some v
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.map_csSup : ∀ {α : Type u} {β : Type v} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
  {f : α → β}, LeftOrdContinuous f → ∀ {s : Set α}, s.Nonempty → BddAbove s → f (sSup s) = sSup (f '' s)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `HasSumUniformlyOn f g s` means that the (potentially infinite) sum `∑' i, f i b`
for `b : β` converges uniformly on `s` to `g`.  -/
HasSumUniformlyOn : {α : Type u_1} →
  {β : Type u_2} → {ι : Type u_3} → [AddCommMonoid α] → (ι → β → α) → (β → α) → Set β → [UniformSpace α] → Prop
-- Mathlib.Algebra.Ring.Associator
associator_op : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (x y z : Rᵐᵒᵖ),
  associator x y z = -MulOpposite.op (associator (MulOpposite.unop z) (MulOpposite.unop y) (MulOpposite.unop x))
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.IsDynCoverOf.union : ∀ {X : Type u_1} {T : X → X} {F G s t : Set X} {U : SetRel X X} {n : ℕ},
  Dynamics.IsDynCoverOf T F U n s → Dynamics.IsDynCoverOf T G U n t → Dynamics.IsDynCoverOf T (F ∪ G) U n (s ∪ t)
-- Mathlib.GroupTheory.Congruence.Defs
/-- A version of `Quotient.hrecOn₂'` for quotients by `AddCon`.  -/
AddCon.hrecOn₂ : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Add M] →
      [inst_1 : Add N] →
        {cM : AddCon M} →
          {cN : AddCon N} →
            {φ : cM.Quotient → cN.Quotient → Sort u_4} →
              (a : cM.Quotient) →
                (b : cN.Quotient) →
                  (f : (x : M) → (y : N) → φ ↑x ↑y) →
                    (∀ (x : M) (y : N) (x' : M) (y' : N), cM x x' → cN y y' → f x y ≍ f x' y') → φ a b
-- Mathlib.Algebra.Algebra.Pi
/-- Use `AlgHom.pi` instead.  -/
Pi.algHom : {ι : Type u_1} →
  (R : Type u_2) →
    (A : ι → Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → Semiring (A i)] →
          [inst_2 : (i : ι) → Algebra R (A i)] →
            {B : Type u_4} →
              [inst_3 : Semiring B] → [inst_4 : Algebra R B] → ((i : ι) → B →ₐ[R] A i) → B →ₐ[R] (i : ι) → A i