mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_filter_not_contains_map_fst_of_contains_eq_false_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = false →
      Std.Internal.List.getValue? k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) =
        Std.Internal.List.getValue? k l₁
-- Mathlib.FieldTheory.SeparablyGenerated
MvPolynomial.coeff_toPolynomialAdjoinImageCompl_ne_zero : ∀ {k : Type u_1} {K : Type u_2} {ι : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {a : ι → K}
  {F : MvPolynomial ι k},
  (∀ (F' : MvPolynomial ι k), F' ≠ 0 → (MvPolynomial.aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree) →
    ∀ σ ∈ F.support, ∀ (i : ι), σ i ≠ 0 → (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) ≠ 0
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
LinearIsometryEquiv.integrable_comp_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} {H : Type u_9}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup H] {𝕜 : Type u_10} {𝕜' : Type u_11}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜' E]
  [inst_5 : NormedSpace 𝕜 H] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [RingHomIsometric σ] [RingHomIsometric σ']
  [inst_8 : RingHomInvPair σ σ'] [inst_9 : RingHomInvPair σ' σ] {φ : α → H} (L : H ≃ₛₗᵢ[σ] E),
  MeasureTheory.Integrable (fun a => L (φ a)) μ ↔ MeasureTheory.Integrable φ μ
-- Mathlib.MeasureTheory.Group.Convolution
/-- To get commutativity, we need the underlying addition to be commutative.  -/
MeasureTheory.Measure.conv_comm : ∀ {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M]
  (μ ν : MeasureTheory.Measure M) [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν], μ.conv ν = ν.conv μ
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.FunctionData.mk.inj : ∀ {lctx : Lean.LocalContext} {insts : Lean.LocalInstances} {fn : Lean.Expr} {args : Array Mathlib.Meta.FunProp.Mor.Arg}
  {mainVar : Lean.Expr} {mainArgs : Array ℕ} {lctx_1 : Lean.LocalContext} {insts_1 : Lean.LocalInstances}
  {fn_1 : Lean.Expr} {args_1 : Array Mathlib.Meta.FunProp.Mor.Arg} {mainVar_1 : Lean.Expr} {mainArgs_1 : Array ℕ},
  { lctx := lctx, insts := insts, fn := fn, args := args, mainVar := mainVar, mainArgs := mainArgs } =
      { lctx := lctx_1, insts := insts_1, fn := fn_1, args := args_1, mainVar := mainVar_1, mainArgs := mainArgs_1 } →
    lctx = lctx_1 ∧ insts = insts_1 ∧ fn = fn_1 ∧ args = args_1 ∧ mainVar = mainVar_1 ∧ mainArgs = mainArgs_1
-- Mathlib.NumberTheory.SiegelsLemma
_private.Mathlib.NumberTheory.SiegelsLemma.0.Int.Matrix.image_T_subset_S : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (A : Matrix α β ℤ) [inst_2 : DecidableEq α]
  [inst_3 : DecidableEq β],
  ∀
    v ∈
      Finset.Icc 0 fun x =>
        ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊,
    A.mulVec v ∈
      Finset.Icc
        (fun i =>
          ∑ j,
            ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ *
              -(A i j)⁻)
        fun i =>
        ∑ j,
          ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ * (A i j)⁺
-- Mathlib.Analysis.CStarAlgebra.Unitization
_private.Mathlib.Analysis.CStarAlgebra.Unitization.0.«term_⋆» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Star.Module
skewAdjointPart_comp_subtype_skewAdjoint : ∀ (R : Type u_1) {A : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2], skewAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype = LinearMap.id
-- Init.Data.String.Subslice
_private.Init.Data.String.Subslice.0.String.Slice.toSubslice.eq_1 : ∀ (s : String.Slice), s.toSubslice = s.subslice s.startPos s.endPos ⋯
-- Mathlib.Analysis.Normed.Algebra.QuaternionExponential
/-- The closed form for the quaternion exponential on arbitrary quaternions.  -/
Quaternion.exp_eq : ∀ (q : Quaternion ℝ),
  NormedSpace.exp q = NormedSpace.exp q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.instCoeSortType : CoeSort Semigrp (Type u)
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.norm_sq_eq : ∀ {𝕜 : Type u_7} [inst : RCLike 𝕜] {n : Type u_8} [inst_1 : Fintype n] (x : EuclideanSpace 𝕜 n),
  ‖x‖ ^ 2 = ∑ i, ‖x.ofLp i‖ ^ 2
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {v : β}, Std.DTreeMap.Const.get? t k = some v ↔ ∃ k', cmp k k' = Ordering.eq ∧ (k', v) ∈ Std.DTreeMap.Const.toArray t
-- Mathlib.Analysis.Convex.Deriv
StrictConvexOn.derivWithin_lt_slope : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  StrictConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f S x → derivWithin f S x < slope f x y
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.ofObj_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (M : ↑(F.obj { as := Opposite.op S })) (Y : C) (q : Y ⟶ S) (i₁ i₂ : ι)
  (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
  (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
  (CategoryTheory.Pseudofunctor.DescentData.ofObj M).hom q f₁ f₂ hf₁ hf₂ =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' (f i₁).op.toLoc f₁.op.toLoc q.op.toLoc ⋯).inv.toNatTrans.app M)
      ((F.mapComp' (f i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.toNatTrans.app M)
-- Mathlib.Data.Finset.Basic
Finset.filter_insert : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] [inst_1 : DecidableEq α] (a : α) (s : Finset α),
  Finset.filter p (insert a s) = if p a then insert a (Finset.filter p s) else Finset.filter p s
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivRight_X_some : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (x : S₁),
  (MvPolynomial.optionEquivRight R S₁) (MvPolynomial.X (some x)) = MvPolynomial.X x
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instBot : {α : Type u_1} → [inst : TopologicalSpace α] → Bot (TopologicalSpace.Compacts α)
-- Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
/-- If there exists `ε > 0` such that the local integral curve at each point `x : M` is defined at
least on an open interval `Ioo (-ε) ε`, then every point on `M` has a global integral curve
passing through it.

See Lemma 9.15, [J.M. Lee (2012)][lee2012].  -/
exists_isMIntegralCurve_of_isMIntegralCurveOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] [T2Space M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x},
  (ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) →
    ∀ {ε : ℝ},
      0 < ε →
        (∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Set.Ioo (-ε) ε)) →
          ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurve γ v
-- Mathlib.Algebra.CubicDiscriminant
Cubic.leadingCoeff_of_c_ne_zero' : ∀ {R : Type u_1} {c d : R} [inst : Semiring R], c ≠ 0 → { a := 0, b := 0, c := c, d := d }.toPoly.leadingCoeff = c
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_one : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : NonAssocSemiring α] [inst_2 : StarRing α],
  Matrix.conjTranspose 1 = 1
-- Mathlib.Analysis.Convex.Mul
ConcaveOn.mul_convexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E] [inst_6 : AddCommGroup G] [inst_7 : Module 𝕜 G]
  [inst_8 : Module 𝕜 E] {s : Set G} [IsOrderedModule 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f g : G → E},
  ConcaveOn 𝕜 s f →
    ConvexOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x) → (∀ ⦃x : G⦄, x ∈ s → g x ≤ 0) → MonovaryOn f g s → ConvexOn 𝕜 s (f * g)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInsertReplaceEdit : Lean.FromJson Lean.Lsp.InsertReplaceEdit
-- Mathlib.Order.Bounds.Basic
IsGreatest.unique : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {a b : α}, IsGreatest s a → IsGreatest s b → a = b
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.nondegenerate_toMatrix₂'_iff : ∀ {R : Type u_1} {n : Type u_11} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] {B : (m → R) →ₗ[R] (n → R) →ₗ[R] R},
  ((LinearMap.toMatrix₂' R) B).Nondegenerate ↔ B.Nondegenerate
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.toAdditiveBialgEquiv_single : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  [inst_3 : Monoid M] (m : M) (a : A),
  (MonoidAlgebra.toAdditiveBialgEquiv R A M) (MonoidAlgebra.single m a) = AddMonoidAlgebra.single (Additive.ofMul m) a
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s t : Set X),
  SeparatedNhds s t = ∃ U V, IsOpen U ∧ IsOpen V ∧ s ⊆ U ∧ t ⊆ V ∧ Disjoint U V
-- Mathlib.Algebra.Group.WithOne.Map
WithOne.map₂_coe_coe : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β), WithOne.map₂ f ↑a ↑b = ↑(f a b)
-- Init.Data.List.Monadic
List.forIn'_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [inst : Monad m] [LawfulMonad m]
  {l : List α} (g : α → β) (f : (b : β) → b ∈ List.map g l → γ → m (ForInStep γ)),
  forIn' (List.map g l) init f = forIn' l init fun a h y => f (g a) ⋯ y
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The obvious functor `(WidePullbackShape J)ᵒᵖ ⥤ WidePushoutShape J`  -/
CategoryTheory.Limits.widePullbackShapeUnop : (J : Type w) →
  CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ (CategoryTheory.Limits.WidePushoutShape J)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.Fan.proj.eq_1 : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C} (p : CategoryTheory.Limits.Fan f)
  (j : β), p.proj j = p.π.app { as := j }
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.ι_π_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C) (X : C), CategoryTheory.CategoryStruct.comp (Φ.ι.app X) (Φ.π.app X) = 0
-- Mathlib.Order.SuccPred.Limit
Order.not_isPredLimit_pred_of_not_isMin : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : PredOrder α], ¬IsMin a → ¬Order.IsPredLimit (Order.pred a)
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.isZero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n₀ n₁ : ℤ),
  autoParam (n₀ < n₁) CategoryTheory.Triangulated.TStructure.isZero._auto_1 →
    ∀ [t.IsLE X n₀] [t.IsGE X n₁], CategoryTheory.Limits.IsZero X
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.digits_append_digits : ∀ {b m n : ℕ}, 0 < b → b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.instModulePolynomial : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          (a : A) →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : Module A M] →
                  [inst_5 : Module R M] → [inst_6 : IsScalarTower R A M] → Module (Polynomial R) (Module.AEval R M a)
-- Init.Data.Int.Order
Int.mul.eq_4 : ∀ (m_2 n_2 : ℕ), (Int.negSucc m_2).mul (Int.negSucc n_2) = Int.ofNat (m_2.succ * n_2.succ)
-- Mathlib.Topology.Order.IntermediateValue
Continuous.image_Ioo_of_strictMono : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ}, Continuous f → StrictMono f → f '' Set.Ioo a b = Set.Ioo (f a) (f b)
-- Init.Data.List.Nat.TakeDrop
List.take_append_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, List.take l₁.length (l₁ ++ l₂) = l₁
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.MatcherInfo.getMotivePos : Lean.Meta.MatcherInfo → ℕ
-- Mathlib.Algebra.Group.Subgroup.Basic
AddAut.characteristic_apply_apply_coe : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : H.Characteristic] (φ : AddAut G) (h : ↥H),
  ↑(((AddAut.characteristic H) φ) h) = φ ↑h
-- Mathlib.RingTheory.Conductor
conductor_eq_top_of_adjoin_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  R[x] = ⊤ → conductor R x = ⊤
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.mem_addUnits_iff : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) (x : AddUnits M), x ∈ S.addUnits ↔ ↑x ∈ S ∧ ↑(-x) ∈ S
-- Init.Data.List.Basic
List.reverseAux.eq_1 : ∀ {α : Type u} (x : List α), [].reverseAux x = x
-- Init.GrindInstances.ToInt
Lean.Grind.instMulFinCoOfNatIntCast : ∀ {n : ℕ}, Lean.Grind.ToInt.Mul (Fin n) (Lean.Grind.IntInterval.co 0 ↑n)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.AllZero.replicate : ∀ {n : ℕ}, Tactic.ComputeAsymptotics.UnitMonomial.AllZero (List.replicate n 0)
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_mem_unitary_of_mem_skewAdjoint : ∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] [inst_3 : StarRing 𝔸] [ContinuousStar 𝔸]
  {x : 𝔸}, x ∈ skewAdjoint 𝔸 → NormedSpace.exp x ∈ unitary 𝔸
-- Mathlib.Combinatorics.Graph.Delete
/-- Delete a set `F` of edges from `G`. This is a special case of `restrict`,
but we define it with `copy` so that the edge set is definitionally equal to `E(G) \ F`.  -/
Graph.deleteEdges : {α : Type u_1} → {β : Type u_2} → Graph α β → Set β → Graph α β
-- Lean.Parser.Term
Lean.Parser.Term.forInMacro : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraDualNumber.equiv_ι : ∀ {R : Type u_1} [inst : CommRing R] (r : R),
  CliffordAlgebraDualNumber.equiv ((CliffordAlgebra.ι 0) r) = r • DualNumber.eps
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
RingHom.isLocalHom_comp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Semiring T]
  (g : S →+* T) (f : R →+* S) [IsLocalHom g] [IsLocalHom f], IsLocalHom (g.comp f)
-- Batteries.Data.String.Lemmas
String.findAux_of_valid : ∀ (p : Char → Bool) (l m r : List Char),
  String.Legacy.findAux (String.ofList (l ++ m ++ r)) p { byteIdx := String.utf8Len l + String.utf8Len m }
      { byteIdx := String.utf8Len l } =
    { byteIdx := String.utf8Len l + String.utf8Len (List.takeWhile (fun x => !p x) m) }
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_union : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  Disjoint s t → MeasurableSet t → μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsInverseImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor D C) [P.IsClosedUnderIsomorphisms],
  (P.inverseImage F).IsClosedUnderIsomorphisms
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- Each vector space has a basis.  -/
Module.Basis.ofVectorSpace : (K : Type u_3) →
  (V : Type u_4) →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Module.Basis (↑(Module.Basis.ofVectorSpaceIndex K V)) K V
-- Mathlib.Probability.Martingale.OptionalSampling
/-- If `τ` and `σ` are two stopping times with `σ ≤ τ` and `τ` is bounded, then the value of a
martingale `f` at `σ` is the conditional expectation of its value at `τ` with respect to the
σ-algebra generated by `σ`.  -/
MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le : ∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : TopologicalSpace ι]
  [OrderTopology ι] {ℱ : MeasureTheory.Filtration ι m} [MeasureTheory.SigmaFiniteFiltration μ ℱ] {τ σ : Ω → WithTop ι}
  {f : ι → Ω → E} {n : ι} [inst_7 : Nonempty ι] [Countable ι],
  MeasureTheory.Martingale f ℱ μ →
    MeasureTheory.IsStoppingTime ℱ τ →
      ∀ (hσ : MeasureTheory.IsStoppingTime ℱ σ),
        σ ≤ τ →
          (∀ (x : Ω), τ x ≤ ↑n) →
            ∀ [MeasureTheory.SigmaFinite (μ.trim ⋯)],
              MeasureTheory.stoppedValue f σ =ᵐ[μ] μ[MeasureTheory.stoppedValue f τ | hσ.measurableSpace]
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- Summand in the series for the Fréchet derivative of the Jacobi theta function.  -/
jacobiTheta₂_term_fderiv : ℤ → ℂ → ℂ → ℂ × ℂ →L[ℂ] ℂ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Polynomial.Chebyshev.chebyshevTsequence.eq_1 : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : NeZero 2],
  Polynomial.Chebyshev.chebyshevTsequence R = { elems' := fun n => Polynomial.Chebyshev.T R ↑n, degree_eq' := ⋯ }
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.MorphismProperty.instCategoryLocalization : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (W : CategoryTheory.MorphismProperty C) → CategoryTheory.Category.{max u_1 u_2, u_1} W.Localization
-- Lean.Meta.Instances
Lean.Meta.instInhabitedDefaultInstances : Inhabited Lean.Meta.DefaultInstances
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.InductionCandidate.mk.sizeOf_spec : ∀ (fvarId : Lean.FVarId) (val : Lean.InductiveVal),
  sizeOf { fvarId := fvarId, val := val } = 1 + sizeOf fvarId + sizeOf val
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- For natural numbers `n`, the proximity function of `f ^ n` at `⊤` equals `n` times the proximity
function of `f` at `⊤`.
 -/
ValueDistribution.proximity_pow_top : ∀ {f : ℂ → ℂ} {n : ℕ}, ValueDistribution.proximity (f ^ n) ⊤ = n • ValueDistribution.proximity f ⊤
-- Mathlib.Data.Nat.PSub
_private.Mathlib.Data.Nat.PSub.0.Nat.ppred.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instLTOffset : LT Std.Time.Minute.Offset
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.instModuleDirectSum : {I : Type u} →
  (R : Type v) →
    [inst : CommSemiring R] →
      (A : I → Type w) →
        [inst_1 : (i : I) → Semiring (A i)] → [(i : I) → Algebra R (A i)] → Module R (DirectSum I fun i => A i)
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.isEmbedding_restrict : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  Topology.IsEmbedding (e.source.domRestrict ↑e.toPartialEquiv)
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.stM : Lean.Elab.Do.ControlStack → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.instEquivLike : {R : Type u_4} →
  {S : Type u_5} → [inst : Mul R] → [inst_1 : Mul S] → [inst_2 : Add R] → [inst_3 : Add S] → EquivLike (R ≃+* S) R S
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Flattening with the inner combination specialized to `convexCombPair`.  -/
Convexity.iConvexComb_convexCombPair : ∀ {R : Type u_1} {M : Type u_3} {I : Type u_6} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] (s t : I → R) (hs : ∀ (i : I), 0 ≤ s i)
  (ht : ∀ (i : I), 0 ≤ t i) (h : ∀ (i : I), s i + t i = 1) (f : Convexity.StdSimplex R I) (m₁ m₂ : I → M),
  (Convexity.iConvexComb f fun i => Convexity.convexCombPair (s i) (t i) ⋯ ⋯ ⋯ (m₁ i) (m₂ i)) =
    Convexity.sConvexComb (Convexity.iConvexComb f fun i => Convexity.StdSimplex.duple (m₁ i) (m₂ i) ⋯ ⋯ ⋯)
-- Mathlib.Order.Category.BoolAlg
_private.Mathlib.Order.Category.BoolAlg.0.BoolAlg.Hom.mk.inj : ∀ {X Y : BoolAlg} {hom' hom'_1 : BoundedLatticeHom ↑X ↑Y}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPair_obj_zero : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y),
  (CategoryTheory.Limits.parallelPair f g).obj CategoryTheory.Limits.WalkingParallelPair.zero = X
-- Mathlib.RingTheory.Localization.FractionRing
/-- Taking fraction ring is idempotent: a fraction ring of a fraction ring of `R` is
itself a fraction ring of `R`.  -/
IsFractionRing.trans : ∀ (R : Type u_1) [inst : CommRing R] (K : Type u_5) [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K]
  (L : Type u_6) [inst_4 : CommRing L] [inst_5 : Algebra K L] [IsFractionRing K L] [inst_7 : Algebra R L]
  [IsScalarTower R K L], IsFractionRing R L
-- Aesop.Forward.Match
/-- Given a complete match `m` for `r`, get arguments to `r` contained in the
match's slots and substitution. For non-immediate arguments, we return `none`.
The returned levels are suitable assignments for the level mvars of `r`.  -/
Aesop.CompleteMatch.reconstructArgs : Aesop.ForwardRule → Aesop.CompleteMatch → Array (Option Lean.Expr) × Array (Option Lean.Level)
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.openCell_subset_of_mem`. -/
Topology.CWComplex.Subcomplex.openCell_subset_of_mem : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n},
  i ∈ E.I n → Topology.RelCWComplex.openCell n i ⊆ ↑E
-- Mathlib.Algebra.Algebra.Equiv
RingEquiv.equivNatAlgEquiv_symm_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : Semiring R] [inst_1 : Semiring S] (self : R ≃ₐ[ℕ] S),
  (RingEquiv.equivNatAlgEquiv R S).symm self = self.toRingEquiv
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolParams.mk.sizeOf_spec : ∀ (textDocument : Lean.Lsp.TextDocumentIdentifier), sizeOf { textDocument := textDocument } = 1 + sizeOf textDocument
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get!.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited β] (m m_1 : Std.ExtHashMap α β), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.get! a = m_1.get! a_1
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.mem_localized' : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] (M' : Submodule R M) (x : N),
  x ∈ Submodule.localized' S p f M' ↔ ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x