mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Basic
/-- Replaces the element at the given index, if it exists, with the result of applying `f` to it. If the
index is invalid, the array is returned unmodified.

Examples:
 * `#[1, 2, 3].modify 0 (· * 10) = #[10, 2, 3]`
 * `#[1, 2, 3].modify 2 (· * 10) = #[1, 2, 30]`
 * `#[1, 2, 3].modify 3 (· * 10) = #[1, 2, 3]`
 -/
Array.modify : {α : Type u} → Array α → ℕ → (α → α) → Array α
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.instInhabitedAppImplicitArg : Inhabited Lean.PrettyPrinter.Delaborator.AppImplicitArg
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.closed : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C), IsClosed ↑E
-- Init.Data.Iterators.Basic
Std.IterStep.successor_yield : ∀ {α : Type u} {β : Type w} {it : α} {out : β}, (Std.IterStep.yield it out).successor = some it
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
HomogeneousIdeal.map_map : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {σ : Type u_4} {τ : Type u_5} {ω : Type u_6} {ι : Type u_7}
  [inst : Semiring A] [inst_1 : Semiring B] [inst_2 : Semiring C] [inst_3 : SetLike σ A] [inst_4 : SetLike τ B]
  [inst_5 : SetLike ω C] [inst_6 : AddSubmonoidClass σ A] [inst_7 : AddSubmonoidClass τ B]
  [inst_8 : AddSubmonoidClass ω C] [inst_9 : DecidableEq ι] [inst_10 : AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ω}
  [inst_11 : GradedRing 𝒜] [inst_12 : GradedRing ℬ] [inst_13 : GradedRing 𝒞] (f : 𝒜 →+*ᵍ ℬ) (g : ℬ →+*ᵍ 𝒞)
  {I : HomogeneousIdeal 𝒜}, HomogeneousIdeal.map g (HomogeneousIdeal.map f I) = HomogeneousIdeal.map (g.comp f) I
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- The linear isometric equivalence implementing identifying the Hilbert space with `ℓ²`.  -/
HilbertBasis.repr : {ι : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : RCLike 𝕜] →
      {E : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] → HilbertBasis ι 𝕜 E → E ≃ₗᵢ[𝕜] ↥(lp (fun x => 𝕜) 2)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivAt.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (f : E → F) (f' : F)
  (x v : E), HasLineDerivAt 𝕜 f f' x v = HasDerivAt (fun t => f (x + t • v)) f' 0
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
EuclideanSpace.restrict₂.congr_simp : ∀ {ι' : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {I J : Finset ι'} (hIJ : I ⊆ J),
  EuclideanSpace.restrict₂ hIJ = EuclideanSpace.restrict₂ hIJ
-- Init.Data.String.Lemmas.Slice
String.Pos.get?_eq_none : ∀ {s : String} {p : s.Pos}, p = s.endPos → p.get? = none
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- The additive congruence relation defined by the kernel of an additive group homomorphism is
equal to its kernel as an additive congruence relation.  -/
QuotientAddGroup.con_ker_eq_addConKer : ∀ {G : Type u_1} {M : Type u_4} [inst : AddGroup G] [inst_1 : AddMonoid M] (f : G →+ M),
  QuotientAddGroup.con f.ker = AddCon.ker f
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
/-- The homomorphism from π₁(X, x) to π₁(Y, y) induced by a continuous map `f` with `f x = y`.  -/
FundamentalGroup.mapOfEq : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (f : C(X, Y)) → {x : X} → {y : Y} → f x = y → FundamentalGroup X x →* FundamentalGroup Y y
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
CategoryTheory.LocalizerMorphism.RightResolution.mk.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {X₁ : C₁}
  (w w_1 : X₂ ⟶ Φ.functor.obj X₁) (e_w : w = w_1) (hw : W₂ w),
  { X₁ := X₁, w := w, hw := hw } = { X₁ := X₁, w := w_1, hw := ⋯ }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.Cache.get?.match_1.eq_2 : ∀ {w : ℕ} (expr : Std.Tactic.BVDecide.BVExpr w)
  (motive : Option (Vector Std.Sat.AIG.Fanin { w := w, expr := expr }.w) → Sort u_1)
  (h_1 : (refs : Vector Std.Sat.AIG.Fanin { w := w, expr := expr }.w) → none = some refs → motive (some refs))
  (h_2 : none = none → motive none),
  (match h : none with
    | some refs => h_1 refs h
    | none => h_2 h) =
    h_2 ⋯
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.extendScalars_sup : ∀ {K : Type u_1} [inst : Field K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  {F E E' : IntermediateField K L} (h : F ≤ E) (h' : F ≤ E'),
  IntermediateField.extendScalars h ⊔ IntermediateField.extendScalars h' = IntermediateField.extendScalars ⋯
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.Context.pattern : Lean.Meta.Sym.UnifyM.Context✝ → Lean.Meta.Sym.Pattern
-- Mathlib.Order.Heyting.Basic
Prod.instCompl : {α : Type u_2} → {β : Type u_3} → [Compl α] → [Compl β] → Compl (α × β)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Let `t := g ^ d / f ^ e`, then `A_{(fg)} = A_{(f)}[1/t]`.  -/
HomogeneousLocalization.Away.isLocalization_mul : ∀ {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {e d : ℕ} {f : A} (hf : f ∈ 𝒜 d) {g : A} (hg : g ∈ 𝒜 e) {x : A} (hx : x = f * g),
  d ≠ 0 → IsLocalization.Away (HomogeneousLocalization.Away.isLocalizationElem hf hg) (HomogeneousLocalization.Away 𝒜 x)
-- Mathlib.Order.Partition.Finpartition
instDecidableEqFinpartition.decEq : {α : Type u_2} →
  {inst : Lattice α} →
    {inst_1 : OrderBot α} → {a : α} → [DecidableEq α] → (x x_1 : Finpartition a) → Decidable (x = x_1)
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.Tendsto.prod_map_prod_atBot : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder γ] {F : Filter α} {G : Filter β} {f : α → γ}
  {g : β → γ},
  Filter.Tendsto f F Filter.atBot →
    Filter.Tendsto g G Filter.atBot → Filter.Tendsto (Prod.map f g) (F ×ˢ G) Filter.atBot
-- Init.Data.Nat.Basic
Nat.instAssociativeHAdd : Std.Associative fun x1 x2 => x1 + x2
-- Mathlib.Algebra.Ring.CentroidHom
/-- `CentroidHom.toEnd` as a `RingHom`.  -/
CentroidHom.toEndRingHom : (α : Type u_5) → [inst : NonUnitalNonAssocSemiring α] → CentroidHom α →+* AddMonoid.End α
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arcsin`, version subtracting vectors.  -/
InnerProductGeometry.angle_sub_eq_arcsin_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x ≠ 0 ∨ y ≠ 0 → InnerProductGeometry.angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)
-- Init.Data.List.Lemmas
List.not_mem_of_not_mem_cons : ∀ {α : Type u_1} {a b : α} {l : List α}, a ∉ b :: l → a ∉ l
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.p : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Int.Internal.Linear.Poly
-- Mathlib.CategoryTheory.Localization.Bousfield
/-- The bijection `(Y ⟶ Z) ≃ (X ⟶ Z)` induced by `f : X ⟶ Y` when `P.isLocal f`
and `P Z`.  -/
CategoryTheory.ObjectProperty.isLocal.homEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P : CategoryTheory.ObjectProperty C} → {X Y : C} → {f : X ⟶ Y} → P.isLocal f → (Z : C) → P Z → (Y ⟶ Z) ≃ (X ⟶ Z)
-- Lean.Util.LeanOptions
Lean.LeanOptionValue.ofBool : Bool → Lean.LeanOptionValue
-- Mathlib.Algebra.GroupWithZero.Defs
mul_left_inj' : ∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [IsRightCancelMulZero M₀] {a b c : M₀},
  c ≠ 0 → (a * c = b * c ↔ a = b)
-- Std.Data.String.ToInt
String.toInt?_eq_some_iff : ∀ {s : String} {a : ℤ},
  s.toInt? = some a ↔ (∃ b, s.toNat? = some b ∧ a = ↑b) ∨ ∃ t, s = "-" ++ t ∧ ∃ b, t.toNat? = some b ∧ a = -↑b
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_units_conj' : ∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R] (M : (Matrix m m R)ˣ)
  (N : Matrix m m R), (↑M⁻¹ * N * ↑M).det = N.det
-- Mathlib.GroupTheory.GroupAction.FixedPoints
AddAction.vadd_fixedBy : ∀ (α : Type u_1) {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (g h : G),
  h +ᵥ AddAction.fixedBy α g = AddAction.fixedBy α (h + g + -h)
-- Mathlib.Data.Multiset.AddSub
Multiset.sub_le_self : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s - t ≤ s
-- Init.Data.Int.Order
Int.neg_lt_neg_iff : ∀ {a b : ℤ}, -a < -b ↔ b < a
-- Mathlib.Algebra.Group.Defs
npow_eq_pow : ∀ {M : Type u_2} [inst : Monoid M] (n : ℕ) (x : M), NPow.npow n x = x ^ n
-- Mathlib.RingTheory.Valuation.Integers
Valuation.leIdeal_mono : ∀ {R : Type u} {Γ₀ : Type v} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀),
  Monotone v.leIdeal
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : SizeOf B] [inst_3 : SizeOf C] (toPrelaxFunctorStruct : CategoryTheory.PrelaxFunctorStruct B C)
  (map₂_id :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toPrelaxFunctorStruct.map₂ (CategoryTheory.CategoryStruct.id f) =
          CategoryTheory.CategoryStruct.id (toPrelaxFunctorStruct.map f))
      CategoryTheory.PrelaxFunctor.map₂_id._autoParam)
  (map₂_comp :
    autoParam
      (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
        toPrelaxFunctorStruct.map₂ (CategoryTheory.CategoryStruct.comp η θ) =
          CategoryTheory.CategoryStruct.comp (toPrelaxFunctorStruct.map₂ η) (toPrelaxFunctorStruct.map₂ θ))
      CategoryTheory.PrelaxFunctor.map₂_comp._autoParam),
  sizeOf { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := map₂_id, map₂_comp := map₂_comp } =
    1 + sizeOf toPrelaxFunctorStruct
-- Batteries.Data.List.Basic
/-- `countPBefore p xs i hip` counts the number of `x` in `xs` before the `i`th index for
which `p x = true`.

For example:
```
countPBefore (· < 3) [5, 1, 3, 2, 4, 0, 1, 4] 5 = 2
```
 -/
List.countPBefore : {α : Type u_1} → (α → Bool) → List α → ℕ → ℕ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.foldlM_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.foldlM f init t₁ = Std.DTreeMap.Raw.foldlM f init t₂
-- Mathlib.Algebra.Quaternion
Quaternion.re_equivProd_symm_apply : ∀ (R : Type u_1) [inst : Zero R] [inst_1 : One R] [inst_2 : Neg R] (a : R × R × R × R),
  ((Quaternion.equivProd R).symm a).re = a.1