mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mk_sup_mk : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : α) (ha : a ∈ L) (hb : b ∈ L),
  ⟨a, ha⟩ ⊔ ⟨b, hb⟩ = ⟨a ⊔ b, ⋯⟩
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
smul_sphere' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {c : 𝕜}, c ≠ 0 → ∀ (x : E) (r : ℝ), c • Metric.sphere x r = Metric.sphere (c • x) (‖c‖ * r)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instHasLimit : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}),
  CategoryTheory.Limits.HasLimit F
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.indexEquivAllRoots_apply_coe : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [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)
  [inst_5 : P.EmbeddedG2] [inst_6 : Finite ι] [inst_7 : CharZero R] [inst_8 : IsDomain R] [inst_9 : P.IsIrreducible]
  (i : ι), ↑((RootPairing.EmbeddedG2.indexEquivAllRoots P) i) = P.root i
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- A variant of `iteratedDerivWithin_const_smul` without differentiability assumption when
the scalar multiplication is by division ring elements.  -/
iteratedDerivWithin_const_smul_field : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} {𝕝 : Type u_4} [inst_3 : DivisionSemiring 𝕝]
  [inst_4 : Module 𝕝 F] [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] (c : 𝕝) (f : 𝕜 → F),
  iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x
-- Mathlib.Data.Prod.TProd
/-- Pi-types are equivalent to iterated products.  -/
List.TProd.piEquivTProd : {ι : Type u} →
  {α : ι → Type v} → {l : List ι} → [DecidableEq ι] → l.Nodup → (∀ (i : ι), i ∈ l) → ((i : ι) → α i) ≃ List.TProd α l
-- Mathlib.Algebra.Group.Pi.Basic
Pi.instIsLeftCancelMul : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → Mul (f i)] [∀ (i : I), IsLeftCancelMul (f i)],
  IsLeftCancelMul ((i : I) → f i)
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.biconeMk_obj : ∀ (J : Type v₁) [inst : CategoryTheory.SmallCategory J] {C : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} C]
  {F : CategoryTheory.Functor J C} (c₁ c₂ : CategoryTheory.Limits.Cone F) (X : CategoryTheory.Bicone J),
  (CategoryTheory.biconeMk J c₁ c₂).obj X = CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.tidy.inj : ∀ {s : Lean.Omega.Constraint} {c : Lean.Omega.Coeffs} {j j_1 : Lean.Elab.Tactic.Omega.Justification s c},
  j.tidy = j_1.tidy → j = j_1
-- Mathlib.Algebra.Order.Hom.TypeTags
/-- Reinterpret `G ≃* Multiplicative H` as `Additive G ≃+ H`.  -/
OrderMonoidIso.toAdditiveLeft : {G : Type u_1} →
  {H : Type u_2} →
    [inst : CommMonoid G] →
      [inst_1 : PartialOrder G] →
        [inst_2 : AddCommMonoid H] → [inst_3 : PartialOrder H] → (G ≃*o Multiplicative H) ≃ (Additive G ≃+o H)
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_union_left : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → Set.Ioc a b ∪ {a} = Set.Icc a b
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableAt.sub_iff_left` -/
DifferentiableAt.fun_sub_iff_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {x : E}, DifferentiableAt 𝕜 g x → (DifferentiableAt 𝕜 (fun i => f i - g i) x ↔ DifferentiableAt 𝕜 f x)
-- Init.Data.Array.Find
Array.idxOf?_eq_none_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {a : α}, xs.idxOf? a = none ↔ a ∉ xs
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_sub_iff_add_lt : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b c : α}, a < c - b ↔ a + b < c
-- Mathlib.Logic.Small.Set
small_single : ∀ {α : Type u1} (x : α), Small.{u, u1} ↑{x}
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → k ∉ m₁ ∩ m₂
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Slice.0.String.Slice.find?.match_1.congr_eq_2 : ∀ (s : String.Slice) (motive : String.Slice.Pattern.SearchStep s → Sort u_1) (x : String.Slice.Pattern.SearchStep s)
  (h_1 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched startPos endPos))
  (h_2 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.rejected startPos endPos))
  (startPos endPos : s.Pos),
  x = String.Slice.Pattern.SearchStep.rejected startPos endPos →
    (match x with
      | String.Slice.Pattern.SearchStep.matched startPos endPos => h_1 startPos endPos
      | String.Slice.Pattern.SearchStep.rejected startPos endPos => h_2 startPos endPos) ≍
      h_2 startPos endPos
-- Mathlib.Data.Finsupp.Lex
Finsupp.Lex.orderBot : {α : Type u_1} →
  {N : Type u_2} →
    [inst : LinearOrder α] →
      [inst_1 : AddCommMonoid N] → [inst_2 : PartialOrder N] → [IsBotZeroClass N] → OrderBot (Lex (α →₀ N))
-- Mathlib.Topology.Algebra.Monoid
ContinuousMul.of_nhds_one : ∀ {M : Type u} [inst : Monoid M] [inst_1 : TopologicalSpace M],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 * x2) (nhds 1 ×ˢ nhds 1) (nhds 1) →
    (∀ (x₀ : M), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) →
      (∀ (x₀ : M), nhds x₀ = Filter.map (fun x => x * x₀) (nhds 1)) → ContinuousMul M
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.pi_proj_comp : ∀ {R : Type u_1} [inst : Semiring R] {M₂ : Type u_3} [inst_1 : TopologicalSpace M₂] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M₂] {ι : Type u_4} {φ : ι → Type u_5} [inst_4 : (i : ι) → TopologicalSpace (φ i)]
  [inst_5 : (i : ι) → AddCommMonoid (φ i)] [inst_6 : (i : ι) → Module R (φ i)] (f : M₂ →L[R] (i : ι) → φ i),
  (ContinuousLinearMap.pi fun x => ContinuousLinearMap.proj x ∘SL f) = f
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_monomial : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) {a : R}, a ≠ 0 → ((SkewPolynomial.monomial n) a).support = {n}
-- Mathlib.Order.SupClosed
SupClosed.inter : ∀ {α : Type u_3} [inst : SemilatticeSup α] {s t : Set α}, SupClosed s → SupClosed t → SupClosed (s ∩ t)
-- Mathlib.Data.Multiset.Bind
Multiset.coe_sigma : ∀ {α : Type u_1} {σ : α → Type u_4} (l₁ : List α) (l₂ : (a : α) → List (σ a)),
  ((↑l₁).sigma fun a => ↑(l₂ a)) = ↑(l₁.sigma l₂)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Each pairwise difference is in the `vectorSpan`.  -/
vsub_mem_vectorSpan : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} {p₁ p₂ : P}, p₁ ∈ s → p₂ ∈ s → p₁ -ᵥ p₂ ∈ vectorSpan k s
-- Mathlib.SetTheory.ZFC.Class
Class.coe_subset : ∀ (x y : ZFSet.{u}), ↑x ⊆ ↑y ↔ x ⊆ y
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.OmissionReason.maxSteps.sizeOf_spec : sizeOf Lean.PrettyPrinter.Delaborator.OmissionReason.maxSteps = 1
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Given three nonzero vectors, adding the angles between them in cyclic order, with the second
vector in each angle negated, results in π. If the vectors add to 0, this is a version of the
sum of the angles of a triangle.  -/
Orientation.oangle_add_cyc3_neg_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y z : V},
  x ≠ 0 → y ≠ 0 → z ≠ 0 → o.oangle x (-y) + o.oangle y (-z) + o.oangle z (-x) = ↑Real.pi
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.exists_null_set_measure_lt_of_disjoint : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  Disjoint μ ν → ∀ {ε : NNReal}, 0 < ε → ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε
-- Init.System.IO
IO.instLETaskState : LE IO.TaskState
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.lift.congr_simp : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
  [inst_1 : CategoryTheory.Category.{uD', uD} D] (G G_1 : CategoryTheory.Functor C D) (e_G : G = G_1)
  (hG : W.IsInvertedBy G),
  CategoryTheory.Localization.Construction.lift G hG = CategoryTheory.Localization.Construction.lift G_1 ⋯
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α fun x => β) (k : α) (v : β)
  (ht : t.Balanced),
  Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew? t k v ht =
    match Std.DTreeMap.Internal.Impl.Const.get? t k with
    | none => (none, (Std.DTreeMap.Internal.Impl.insertIfNew k v t ht).impl)
    | some b => (some b, t)
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Submonoid.LocalizationMap.sec_zero_fst : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  {f : S.LocalizationMap N}, f (f.sec 0).1 = 0
-- Mathlib.Order.Types.Defs
OrderType.type_of_unique : ∀ {α : Type u} [inst : LinearOrder α] [Nonempty α] [Subsingleton α], OrderType.type α = 1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightKind.write : Lean.Lsp.DocumentHighlightKind
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.Consumer.waiter : {α : Type} → Std.CloseableChannel.Bounded.Consumer✝ α → Option (Std.Async.Waiter (Option α))
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_eq_false_iff : ∀ {s : String.Slice} {p : String.Pos.Raw},
  String.Pos.Raw.isValidForSlice s p = false ↔ ¬String.Pos.Raw.IsValidForSlice s p
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.RenameOptions.mk.inj : ∀ {prepareProvider prepareProvider_1 : Bool},
  { prepareProvider := prepareProvider } = { prepareProvider := prepareProvider_1 } →
    prepareProvider = prepareProvider_1
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.subsingleton_hom : ∀ {J : Type u_1}, Quiver.IsThin (CategoryTheory.WithTerminal (CategoryTheory.Discrete J))
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.natCast : {α : Type u} → [inst : Lean.Grind.Semiring α] → ℕ → Lean.Grind.Ring.OfSemiring.Q α
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.set_subsingleton : ∀ {G : Type u_1} [inst : Add G] {A B : Finset G} {a0 b0 : G},
  UniqueAdd A B a0 b0 → {ab | ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 + ab.2 = a0 + b0}.Subsingleton
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_toList_roo : ∀ {m n : ℤ}, (m<...n).toList.toArray = (m<...n).toArray
-- Std.Data.ExtDTreeMap.Basic
/-- Inserts the given mapping into the map. If there is already a mapping for the given key, then both
key and value will be replaced.
 -/
Std.ExtDTreeMap.insert : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → (a : α) → β a → Std.ExtDTreeMap α β cmp
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_add : ∀ (a b : BitVec 8), Int8.ofBitVec (a + b) = Int8.ofBitVec a + Int8.ofBitVec b
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.inv_le_one_iff_one_le : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : Aˣ},
  0 ≤ ↑a → (↑a⁻¹ ≤ 1 ↔ 1 ≤ a)
-- Lean.Elab.PreDefinition.TerminationMeasure
Lean.Elab.TerminationMeasure.mk.injEq : ∀ (ref : Lean.Syntax) (structural : Bool) (fn : Lean.Expr) (ref_1 : Lean.Syntax) (structural_1 : Bool)
  (fn_1 : Lean.Expr),
  ({ ref := ref, structural := structural, fn := fn } = { ref := ref_1, structural := structural_1, fn := fn_1 }) =
    (ref = ref_1 ∧ structural = structural_1 ∧ fn = fn_1)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {S : C} → CategoryTheory.Category.{max v w, max (max (w + 1) u) v} (J.ZeroHypercover S)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_eq_zero_of_ae_eq_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  f =ᵐ[μ] 0 → ∫⁻ (a : α), f a ∂μ = 0
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.eval_whiskerLeft : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g h : b ⟶ c} {η η' : g ⟶ h}
  {θ : CategoryTheory.CategoryStruct.comp f g ⟶ CategoryTheory.CategoryStruct.comp f h},
  η = η' → CategoryTheory.Bicategory.whiskerLeft f η' = θ → CategoryTheory.Bicategory.whiskerLeft f η = θ
-- Mathlib.Topology.IsLocalHomeomorph
/-- The composition of local homeomorphisms is a local homeomorphism.  -/
IsLocalHomeomorph.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {g : Y → Z} {f : X → Y},
  IsLocalHomeomorph g → IsLocalHomeomorph f → IsLocalHomeomorph (g ∘ f)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.Y_eq_of_Y_ne' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → P 1 * Q 2 ^ 3 ≠ W'.negY Q * P 2 ^ 3 → P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
/-- If the inverse of a function `isBigO` to `(|(n : ℝ)| ^ a)⁻¹` for `1 < a`, then the function is
Summable.  -/
EisensteinSeries.summable_inv_of_isBigO_rpow_inv : ∀ {α : Type u_1} [inst : NormedField α] [CompleteSpace α] {f : ℤ → α} {a : ℝ},
  1 < a → ((fun n => (f n)⁻¹) =O[Filter.cofinite] fun n => (|↑n| ^ a)⁻¹) → Summable fun n => (f n)⁻¹
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : SizeOf C] (X : C) [mon : CategoryTheory.MonObj X], sizeOf { X := X, mon := mon } = 1 + sizeOf X + sizeOf mon
-- Mathlib.Order.Circular
/-- A circular preorder is the analogue of a preorder where you can loop around. `≤` and `<` are
replaced by ternary relations `btw` and `sbtw`. `btw` is reflexive and cyclic. `sbtw` is transitive.
 -/
CircularPreorder : Type u_1 → Type u_1
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.d_pos : ∀ {d : ℕ} [dnsq : Zsqrtd.Nonsquare d], 0 < d
-- Std.Http.Data.Status
/-- 431 Request Header Fields Too Large
 -/
Std.Http.Status.requestHeaderFieldsTooLarge : Std.Http.Status
-- Mathlib.Control.Bifunctor
LawfulBifunctor.bimap_bimap : ∀ {F : Type u₀ → Type u₁ → Type u₂} {inst : Bifunctor F} [self : LawfulBifunctor F] {α₀ α₁ α₂ : Type u₀}
  {β₀ β₁ β₂ : Type u₁} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂) (x : F α₀ β₀),
  bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.Map.Arrows.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ φ_1 : CategoryTheory.Functor C D) (e_φ : φ = φ_1) (hφ : Function.Injective φ.obj)
  (S S_1 : CategoryTheory.Subgroupoid C),
  S = S_1 →
    ∀ (c d : D) (a a_1 : c ⟶ d),
      a = a_1 →
        CategoryTheory.Subgroupoid.Map.Arrows φ hφ S c d a = CategoryTheory.Subgroupoid.Map.Arrows φ_1 ⋯ S_1 c d a_1
-- Mathlib.CategoryTheory.Adjunction.Quadruple
CategoryTheory.Adjunction.Quadruple.mk.sizeOf_spec : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} [inst_2 : SizeOf C] [inst_3 : SizeOf D] (adj₁ : L ⊣ F) (adj₂ : F ⊣ G) (adj₃ : G ⊣ R),
  sizeOf { adj₁ := adj₁, adj₂ := adj₂, adj₃ := adj₃ } = 1 + sizeOf adj₁ + sizeOf adj₂ + sizeOf adj₃
-- Std.Sync.Mutex
/-- Creates a new mutex.  -/
Std.Mutex.new : {α : Type} → α → BaseIO (Std.Mutex α)
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- If `v` is a linear independent family of vectors, extend it to a basis indexed by a sum type.  -/
Module.Basis.sumExtend : {ι : Type u_1} →
  {K : Type u_3} →
    {V : Type u_4} →
      [inst : DivisionRing K] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module K V] →
            {v : ι → V} → (hs : LinearIndependent K v) → Module.Basis (ι ⊕ ↑(Module.Basis.sumExtendIndex hs)) K V
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_mul_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R),
  (MvPowerSeries.coeff n) (φ * MvPowerSeries.C a) = (MvPowerSeries.coeff n) φ * a
-- Mathlib.Data.Finset.Interval
Finset.Iio_eq_ssubsets : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), Finset.Iio s = s.ssubsets
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeWhile₂TR.go.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → List α → List β → Sort u_3) (a : α) (as : List α) (b : β)
  (bs : List β) (acca : List α) (accb : List β)
  (h_1 :
    (a : α) →
      (as : List α) →
        (b : β) → (bs : List β) → (acca : List α) → (accb : List β) → motive (a :: as) (b :: bs) acca accb)
  (h_2 : (x : List α) → (x_1 : List β) → (acca : List α) → (accb : List β) → motive x x_1 acca accb),
  (match a :: as, b :: bs, acca, accb with
    | a :: as, b :: bs, acca, accb => h_1 a as b bs acca accb
    | x, x_1, acca, accb => h_2 x x_1 acca accb) =
    h_1 a as b bs acca accb
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Mathlib.Meta.NormNum.IsNNRat.rpow_isNNRat : ∀ (a b : ℝ) (na da : ℕ),
  Mathlib.Meta.NormNum.IsNNRat a na da →
    ∀ (nr dr : ℕ),
      Mathlib.Meta.NormNum.IsNat (↑na ^ b) nr →
        Mathlib.Meta.NormNum.IsNat (↑da ^ b) dr → Mathlib.Meta.NormNum.IsNNRat (a ^ b) nr dr
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α],
  Std.Rxc.instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE =
    { IsPlausibleStep := fun it step => step = Std.Rxc.Iterator.Monadic.step it,
      step := fun it => pure (Std.Shrink.deflate ⟨Std.Rxc.Iterator.Monadic.step it, ⋯⟩) }
-- Mathlib.CategoryTheory.Limits.Types.End
CategoryTheory.Limits.chosenEnd.map_apply : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J]
  {F G : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))} (f : F ⟶ G)
  (x : CategoryTheory.Limits.Types.end_ F),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.chosenEnd.map f)) x =
    ⟨fun j => (CategoryTheory.ConcreteCategory.hom ((f.app (Opposite.op j)).app j)) (↑x j), ⋯⟩
-- Mathlib.Order.Filter.AtTopBot.Interval
Finset.tendsto_Ioc_neg : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [inst_3 : LocallyFiniteOrder R]
  [Archimedean R] [Nontrivial R], Filter.Tendsto (fun n => Finset.Ioc (-↑n) ↑n) Filter.atTop Filter.atTop
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.tensor_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mon C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.card_zero : ∀ {α : Type u_1}, Multiset.card 0 = 0
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.forM_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {n : Type w → Type w''}
  [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad n] [inst_5 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_7 : MonadLiftT m n] [LawfulMonadLiftT m n] {it : Std.IterM m β} {f : β → n PUnit.{w + 1}},
  forM it f = do
    let __do_lift ← liftM it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, property⟩ => do
        f out
        forM it' f
      | ⟨Std.IterStep.skip it', property⟩ => forM it' f
      | ⟨Std.IterStep.done, property⟩ => pure PUnit.unit
-- Init.Core
/-- Monadically iterates over the contents of a collection `xs`, with a local state `b` and the
possibility of early termination.

Because a `do` block supports local mutable bindings along with `return`, and `break`, the monadic
action passed to `ForIn.forIn` takes a starting state in addition to the current element of the
collection and returns an updated state together with an indication of whether iteration should
continue or terminate. If the action returns `ForInStep.done`, then `ForIn.forIn` should stop
iteration and return the updated state. If the action returns `ForInStep.yield`, then
`ForIn.forIn` should continue iterating if there are further elements, passing the updated state
to the action.

More information about the translation of `for` loops into `ForIn.forIn` is available in [the Lean
reference manual](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=monad-iteration-syntax).
 -/
ForIn.forIn : {m : Type u₁ → Type u₂} →
  {ρ : Type u} →
    {α : outParam (Type v)} → [self : ForIn m ρ α] → {β : Type u₁} → ρ → β → (α → β → m (ForInStep β)) → m β
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverExtension.mkInitial : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → IO σ
-- Std.Internal.Do.WP.Basic
_private.Std.Internal.Do.WP.Basic.0.Std.Internal.Do.EStateM.wpInst.match_1.eq_2 : ∀ {ε σ α : Type} (motive : EStateM.Result ε σ α → Sort u_1) (el : ε) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (el : ε) → (s' : σ) → motive (EStateM.Result.error el s')),
  (match EStateM.Result.error el s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error el s' => h_2 el s') =
    h_2 el s'
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The actual `Subalgebra` obtained from an element of a type satisfying `SubsemiringClass` and
`SMulMemClass`.  -/
Subalgebra.ofClass : {S : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : SetLike S A] → [SubsemiringClass S A] → [SMulMemClass S R A] → S → Subalgebra R A
-- Mathlib.Analysis.RCLike.Extend
Module.Dual.re_extendRCLike_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : AddCommGroup F] [inst_2 : Module ℝ F] [inst_3 : Module 𝕜 F]
  [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : Module.Dual ℝ F) (x : F), RCLike.re (fr.extendRCLike x) = fr x
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rii.Internal.forIn'_eq_forIn'_iter : ∀ {α : Type u} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_3 : Std.Rxi.IsAlwaysFinite α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_5 : Monad m]
  {r : Std.Rii α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' (Std.Rii.Internal.iter r) init fun a ha acc => f a ⋯ acc
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.coe_inj : ∀ {V : Type u} {G : SimpleGraph V} {K : Set V} {C D : G.ComponentCompl K}, ↑C = ↑D ↔ C = D
-- Init.Data.Slice.Notation
/-- This typeclass indicates how to obtain slices of elements of `α` over ranges in the index type
`β`, the ranges being left-open right-unbounded.

The type of the resulting slices is `γ`.
 -/
Std.Roi.Sliceable : Type u → outParam (Type v) → outParam (Type w) → Type (max (max u v) w)