mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Equiv.Functor
/-- Apply a bifunctor to a pair of `Equiv`s.  -/
Bifunctor.mapEquiv : {α β : Type u} →
  {α' β' : Type v} →
    (F : Type u → Type v → Type w) → [inst : Bifunctor F] → [LawfulBifunctor F] → α ≃ β → α' ≃ β' → F α α' ≃ F β β'
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α} {h' : k ∈ Std.DTreeMap.Raw.filterMap f t}
  (h : t.WF), (Std.DTreeMap.Raw.filterMap f t).getKey k h' = t.getKey k ⋯
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.bicomp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [inst : TopologicalSpace α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] {f : α → β} {a : α} [inst_3 : Preorder δ] {op : β → γ → δ},
  Relator.LiftFun (fun x1 x2 => x1 ≤ x2) (Relator.LiftFun (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2) op op →
    IsLocalMin f a → ∀ {g : α → γ}, IsLocalMin g a → IsLocalMin (fun x => op (f x) (g x)) a
-- Lean.Expr
Lean.Expr.mkDataForLet : UInt64 → ℕ → UInt32 → Bool → Bool → Bool → Bool → Lean.Expr.Data
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_filter_le : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] (a b c : α),
  Multiset.filter (fun x => c ≤ x) (Multiset.Ico a b) = Multiset.Ico (max a c) b
-- Std.Do.PostCond
_private.Std.Do.PostCond.0.Std.Do.PostShape.args.match_1.eq_2 : ∀ (motive : Std.Do.PostShape → Sort u_2) (σ : Type u_1) (s : Std.Do.PostShape)
  (h_1 : Unit → motive Std.Do.PostShape.pure)
  (h_2 : (σ : Type u_1) → (s : Std.Do.PostShape) → motive (Std.Do.PostShape.arg σ s))
  (h_3 : (ε : Type u_1) → (s : Std.Do.PostShape) → motive (Std.Do.PostShape.except ε s)),
  (match Std.Do.PostShape.arg σ s with
    | Std.Do.PostShape.pure => h_1 ()
    | Std.Do.PostShape.arg σ s => h_2 σ s
    | Std.Do.PostShape.except ε s => h_3 ε s) =
    h_2 σ s
-- Aesop.Tree.State
Aesop.Goal.isProvenByNormalizationNoCache : Aesop.Goal → Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Φ_three : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.Φ 3 = Polynomial.X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq
-- Mathlib.RingTheory.IdealFilter.Basic
/-- Intersecting the left ideal with `K` does not change `IsTorsionQuot` on the right.
In particular, `IsTorsionQuot F L K` need not require `L ≤ K` for it is equivalent to asserting
the quotient `K / (L ⊓ K)` is `F`-torsion.  -/
IdealFilter.isTorsionQuot_inter_left_iff : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A} {L K : Ideal A}, F.IsTorsionQuot (L ⊓ K) K ↔ F.IsTorsionQuot L K
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.comp_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ}
  (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (k : R) (z₂ : CochainComplex.HomComplex.Cochain G K n₂)
  (h : n₁ + n₂ = n₁₂), z₁.comp (k • z₂) h = k • z₁.comp z₂ h
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaKey.mk.inj : ∀ {expr expr_1 : Lean.Expr}, { expr := expr } = { expr := expr_1 } → expr = expr_1
-- Mathlib.Topology.MetricSpace.Thickening
/-- For the equality, see `thickening_cthickening`.  -/
Metric.thickening_cthickening_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} (ε : ℝ),
  0 ≤ δ → ∀ (s : Set α), Metric.thickening ε (Metric.cthickening δ s) ⊆ Metric.thickening (ε + δ) s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_insert_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {k : α} {v : β k}, (m.insert k v).get? k = some v
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.coeff_k.eq_1 : ∀ (p : Int.Internal.Linear.Poly) (x : Int.Internal.Linear.Var),
  p.coeff_k x = Int.Internal.Linear.Poly.rec (fun x => 0) (fun a y x_1 ih => Bool.rec ih a (Nat.beq x y)) p
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
/-- The language of Presburger arithmetic, defined as (0, 1, +).  -/
FirstOrder.Language.presburger : FirstOrder.Language
-- Mathlib.Order.Interval.Finset.Defs
Set.instFintypeIoc : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → (b a : α) → Fintype ↑(Set.Ioc b a)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_iff_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] {a : α}, m.contains a = true ↔ a ∈ m
-- Mathlib.InformationTheory.Hamming
hammingNorm_comp_le_hammingNorm : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {γ : ι → Type u_4}
  [inst_2 : (i : ι) → DecidableEq (γ i)] [inst_3 : (i : ι) → Zero (β i)] [inst_4 : (i : ι) → Zero (γ i)]
  (f : (i : ι) → γ i → β i) {x : (i : ι) → γ i},
  (∀ (i : ι), f i 0 = 0) → (hammingNorm fun i => f i (x i)) ≤ hammingNorm x
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.instFiniteTypeSubtypeMemSubalgebraSubalgebra : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Algebra.EssFiniteType R S], Algebra.FiniteType R ↥(Algebra.EssFiniteType.subalgebra R S)
-- Lean.Elab.InfoTree.Types
Lean.Elab.DelabTermInfo.mk.inj : ∀ {toTermInfo : Lean.Elab.TermInfo} {location? : Option Lean.DeclarationLocation}
  {mkDocString? : Option (Lean.PPContext → IO String)} {explicit : Bool} {toTermInfo_1 : Lean.Elab.TermInfo}
  {location?_1 : Option Lean.DeclarationLocation} {mkDocString?_1 : Option (Lean.PPContext → IO String)}
  {explicit_1 : Bool},
  { toTermInfo := toTermInfo, location? := location?, mkDocString? := mkDocString?, explicit := explicit } =
      { toTermInfo := toTermInfo_1, location? := location?_1, mkDocString? := mkDocString?_1, explicit := explicit_1 } →
    toTermInfo = toTermInfo_1 ∧ location? = location?_1 ∧ mkDocString? = mkDocString?_1 ∧ explicit = explicit_1
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Dense.borel_eq_generateFrom_Ioc_mem_aux : ∀ {α : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {s : Set α},
  Dense s →
    (∀ (x : α), IsTop x → x ∈ s) →
      (∀ (x y : α), x < y → Set.Ioo x y = ∅ → x ∈ s) →
        borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ioc l u = S}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.paste_horiz_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃},
  CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁ →
    CategoryTheory.CategoryStruct.comp h₁₂ v₁₃ = CategoryTheory.CategoryStruct.comp v₁₂ h₂₂ →
      (CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃
          (CategoryTheory.CategoryStruct.comp h₂₁ h₂₂) ↔
        CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ h₂₂)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ofList_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α}, Std.ExtTreeSet.ofList [k] cmp = ∅.insert k
-- Mathlib.Analysis.Normed.Order.Lattice
norm_inf_sub_inf_le_add_norm : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α]
  (a b c d : α), ‖a ⊓ b - c ⊓ d‖ ≤ ‖a - c‖ + ‖b - d‖
-- Mathlib.Algebra.Polynomial.Sequence
/-- The first `m + 1` polynomials of a polynomial sequence span all polynomials of degree `≤ m` if
their leading coefficients are units.  -/
Polynomial.Sequence.span_degreeLE : ∀ {R : Type u_1} [inst : Ring R] (S : Polynomial.Sequence R) {m : ℕ},
  (∀ i ≤ m, IsUnit (↑S i).leadingCoeff) → Submodule.span R (↑S '' Set.Iic m) = Polynomial.degreeLE R ↑m
-- Init.Core
/-- Non-dependent recursor for `HEq`  -/
HEq.ndrec : {α : Sort u2} → {a : α} → {motive : {β : Sort u2} → β → Sort u1} → motive a → {β : Sort u2} → {b : β} → a ≍ b → motive b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ ∩ t₂).getKey! k = t₁.getKey! k
-- Std.Data.HashSet.Basic
/-- Transforms the hash set into an array of elements in some order.  -/
Std.HashSet.toArray : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → Array α
-- Mathlib.Algebra.Symmetrized
SymAlg.mul_def : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Mul α] [inst_2 : One α] [inst_3 : OfNat α 2] [inst_4 : Invertible 2]
  (a b : αˢʸᵐ), a * b = SymAlg.sym (⅟2 * (SymAlg.unsym a * SymAlg.unsym b + SymAlg.unsym b * SymAlg.unsym a))
-- Lean.Structure
Lean.instInhabitedStructureInfo.default : Lean.StructureInfo
-- Mathlib.RingTheory.Polynomial.GaussLemma
Polynomial.IsPrimitive.map_mul_mem_lifts_iff : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsDomain R] [IsGCDMonoid R] {f : Polynomial R},
  f.IsPrimitive →
    ∀ {g : Polynomial K},
      Polynomial.map (algebraMap R K) f * g ∈ Polynomial.lifts (algebraMap R K) ↔ g ∈ Polynomial.lifts (algebraMap R K)
-- Aesop.Stats.Basic
Aesop.instToJsonScriptGenerated : Lean.ToJson Aesop.ScriptGenerated
-- Init.Data.Iterators.Lemmas.Combinators.Take
Std.Iter.atIdxSlow?_take : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Productive α Id] {k l : ℕ} {it : Std.Iter β},
  Std.Iter.atIdxSlow? l (Std.Iter.take k it) = if l < k then Std.Iter.atIdxSlow? l it else none
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.injOn_arcsin : Set.InjOn Real.arcsin (Set.Icc (-1) 1)
-- Std.Http.Transport
Std.Http.Transport.mk : {α : Type} →
  (α → UInt64 → Std.Async.Async (Option ByteArray)) →
    (α → Array ByteArray → Std.Async.Async Unit) →
      (α → UInt64 → Std.Async.Selector (Option ByteArray)) → (α → IO Unit) → Std.Http.Transport α
-- Init.Prelude
/-- The list whose first element is `head`, where `tail` is the rest of the list.
Usually written `head :: tail`.


Conventions for notations in identifiers:

 * The recommended spelling of `::` in identifiers is `cons`.

 * The recommended spelling of `[a]` in identifiers is `singleton`. -/
List.cons : {α : Type u} → α → List α → List α
-- Init.Data.List.Lemmas
List.set_append_left : ∀ {α : Type u_1} {s t : List α} (i : ℕ) (x : α), i < s.length → (s ++ t).set i x = s.set i x ++ t
-- Mathlib.Algebra.Group.Basic
neg_surjective : ∀ {G : Type u_3} [inst : InvolutiveNeg G], Function.Surjective Neg.neg
-- Mathlib.Analysis.Convex.Quasiconvex
AntitoneOn.quasiconcaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {s : Set E} {f : E → β}, AntitoneOn f s → Convex 𝕜 s → QuasiconcaveOn 𝕜 s f
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- A normed field is a model with corners.  -/
Manifold.«term𝓘(_)» : Lean.ParserDescr
-- Mathlib.Algebra.Free
/-- Additive semigroup quotient of an additive magma.  -/
AddMagma.FreeAddSemigroup : (α : Type u) → [Add α] → Type u
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Composing an alternating map with a linear map on the left gives again an alternating map.  -/
LinearMap.compAlternatingMap : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                {ι : Type u_7} →
                  {N₂ : Type u_11} →
                    [inst_5 : AddCommMonoid N₂] →
                      [inst_6 : Module R N₂] → (N →ₗ[R] N₂) → M [⋀^ι]→ₗ[R] N → M [⋀^ι]→ₗ[R] N₂
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_one : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submodule R A),
  M * 1 = M
-- Mathlib.Analysis.LocallyConvex.Montel
MontelSpace.finiteDimensional_of_normedSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace 𝕜] [hM : MontelSpace 𝕜 E], FiniteDimensional 𝕜 E
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryClass.toSemilinearMapClass : ∀ {𝓕 : Type u_11} {R : outParam (Type u_12)} {R₂ : outParam (Type u_13)} {inst : Semiring R} {inst_1 : Semiring R₂}
  {σ₁₂ : outParam (R →+* R₂)} {E : outParam (Type u_14)} {E₂ : outParam (Type u_15)} {inst_2 : SeminormedAddCommGroup E}
  {inst_3 : SeminormedAddCommGroup E₂} {inst_4 : Module R E} {inst_5 : Module R₂ E₂} {inst_6 : FunLike 𝓕 E E₂}
  [self : SemilinearIsometryClass 𝓕 σ₁₂ E E₂], SemilinearMapClass 𝓕 σ₁₂ E E₂
-- Init.Data.Array.Lemmas
Array.pop_append_of_ne_empty : ∀ {α : Type u_1} {xs ys : Array α}, ys ≠ #[] → (xs ++ ys).pop = xs ++ ys.pop
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.span_neg : ∀ {ι : Type u_1} {R : Type u_7} {M : Type u_8} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M} (hli : LinearIndependent R v)
  (h : autoParam (Submodule.span R (Set.range v) = Submodule.span R (Set.range (-v))) Module.Basis.span_neg._auto_1),
  Module.Basis.span ⋯ =
    (Module.Basis.span hli).map
      (LinearEquiv.neg R ≪≫ₗ LinearEquiv.ofEq (Submodule.span R (Set.range v)) (Submodule.span R (Set.range (-v))) h)
-- Init.Data.Option.Lemmas
Option.join_join : ∀ {α : Type u_1} {x : Option (Option (Option α))}, x.join.join = (Option.map Option.join x).join
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_of_mem_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      k ∈ Std.DTreeMap.Raw.Const.insertMany t l → (List.map Prod.fst l).contains k = false → k ∈ t
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
Homeomorph.trans_transOpenPartialHomeomorph : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} {Z' : Type u_6} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace Z'] (e : X ≃ₜ Y) (e' : Y ≃ₜ Z)
  (f'' : OpenPartialHomeomorph Z Z'),
  (e.trans e').transOpenPartialHomeomorph f'' = e.transOpenPartialHomeomorph (e'.transOpenPartialHomeomorph f'')
-- Mathlib.GroupTheory.Perm.ClosureSwap
/-- If a subgroup is generated by transpositions, then a permutation `f` lies in the subgroup if
and only if `f` has finite support and `f x` always lies in the same orbit as `x`.  -/
mem_closure_isSwap : ∀ {α : Type u_2} [inst : DecidableEq α] {S : Set (Equiv.Perm α)},
  (∀ f ∈ S, f.IsSwap) →
    ∀ {f : Equiv.Perm α},
      f ∈ Subgroup.closure S ↔
        (MulAction.fixedBy α f)ᶜ.Finite ∧ ∀ (x : α), f x ∈ MulAction.orbit (↥(Subgroup.closure S)) x
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.coe_iInf : ∀ {G : Type u_1} [inst : Group G] {ι : Sort u_2} {S : ι → Subgroup G}, ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
_private.Mathlib.Analysis.SpecialFunctions.BinaryEntropy.0.Real.tendsto_log_one_sub_sub_log_nhdsGT_atAtop : Filter.Tendsto (fun p => Real.log (1 - p) - Real.log p) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop
-- Mathlib.Analysis.Normed.Module.Bases
/-- The difference operator `P (n + 1) - P n`.  -/
SchauderBasis.succSub : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {X : Type u_2} → [inst_1 : NormedAddCommGroup X] → [inst_2 : NormedSpace 𝕜 X] → (ℕ → X →L[𝕜] X) → ℕ → X →L[𝕜] X
-- Mathlib.Order.BooleanSubalgebra
/-- A Boolean subalgebra of a lattice inherits a supremum.  -/
BooleanSubalgebra.instSupCoe : {α : Type u_2} → [inst : BooleanAlgebra α] → {L : BooleanSubalgebra α} → Max ↥L
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_eq_of_forall_row_eq_smul_add_pred_aux : ∀ {R : Type v} [inst : CommRing R] {n : ℕ} (k : Fin (n + 1)) (c : Fin n → R),
  (∀ (i : Fin n), k < i.succ → c i = 0) →
    ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
      (∀ (j : Fin n.succ), M 0 j = N 0 j) →
        (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
-- Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
MeasureTheory.StronglyMeasurable.measurableSet_exists_tendsto : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace E] [Countable ι]
  {l : Filter ι} [l.IsCountablyGenerated] {f : ι → X → E} [TopologicalSpace.IsCompletelyPseudoMetrizableSpace E],
  (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
    MeasurableSet {x | ∃ c, Filter.Tendsto (fun x_1 => f x_1 x) l (nhds c)}
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoImage_preimage_hom_homOfLE_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens)
  {Z : AlgebraicGeometry.Scheme} (h : ↑U ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.isoImage f ((TopologicalSpace.Opens.map f.base).obj U)).hom
      (CategoryTheory.CategoryStruct.comp (Y.homOfLE ⋯) h) =
    CategoryTheory.CategoryStruct.comp (f ∣_ U) h
-- Batteries.Data.List.Lemmas
/-- **Alias** of `List.getElem?_set_of_lt`. -/
List.get?_set_of_lt : ∀ {α : Type u_1} (a : α) {m n : ℕ} (l : List α), n < l.length → (l.set m a)[n]? = if m = n then some a else l[n]?
-- Mathlib.Topology.NhdsWithin
frequently_nhds_subtype_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : Set α) (a : ↑s) (P : α → Prop),
  (∃ᶠ (x : ↑s) in nhds a, P ↑x) ↔ ∃ᶠ (x : α) in nhdsWithin (↑a) s, P x
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.map_comp : ∀ {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (α i)]
  [inst_1 : (i : ι) → AddCommMonoid (β i)] (f : (i : ι) → α i →+ β i) {γ : ι → Type u_6}
  [inst_2 : (i : ι) → AddCommMonoid (γ i)] (g : (i : ι) → β i →+ γ i),
  (DirectSum.map fun i => (g i).comp (f i)) = (DirectSum.map g).comp (DirectSum.map f)
-- Mathlib.Data.Nat.SuccPred
Nat.pred_eq_pred : Order.pred = Nat.pred
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.trivialCofibrations_sub_cofibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.trivialCofibrations C ≤ HomotopicalAlgebra.cofibrations C
-- Lean.Util.LeanOptions
Lean.LeanOption.mk.inj : ∀ {name : Lean.Name} {value : Lean.LeanOptionValue} {name_1 : Lean.Name} {value_1 : Lean.LeanOptionValue},
  { name := name, value := value } = { name := name_1, value := value_1 } → name = name_1 ∧ value = value_1
-- Mathlib.Data.EReal.Basic
/-- Extension for the `positivity` tactic: projection from `EReal` to `ℝ`.

We prove that `EReal.toReal x` is nonnegative whenever `x` is nonnegative.
Since `EReal.toReal ⊤ = 0`, we cannot prove a stronger statement,
at least without relying on a tactic like `finiteness`.  -/
Mathlib.Meta.Positivity.evalERealToReal : Mathlib.Meta.Positivity.PositivityExt
-- Init.Data.Array.Range
Array.fst_mem_of_mem_zipIdx : ∀ {α : Type u_1} {x : α × ℕ} {xs : Array α} {k : ℕ}, x ∈ xs.zipIdx k → x.1 ∈ xs
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_balance : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced)
  (hrb : r.Balanced)
  (hlr :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size ∨
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size),
  (Std.DTreeMap.Internal.Impl.balance k v l r hlb hrb hlr).size = l.size + 1 + r.size
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.sub_iff_right : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a₁ a₂ b₁ b₂ : G},
  a₂ ≡ b₂ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p])
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_mem_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α} {a : α}, -a ∈ -s ↔ a ∈ s
-- Lean.Data.Lsp.Basic
/-- The edits to apply.  -/
Lean.Lsp.ApplyWorkspaceEditParams.edit : Lean.Lsp.ApplyWorkspaceEditParams → Lean.Lsp.WorkspaceEdit
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum of pairwise subtractions, where the point on the right is constant and the
sum of the weights is 1.  -/
Finset.sum_smul_vsub_const_eq_affineCombination_vsub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ : ι → P) (p₂ : P),
  ∑ i ∈ s, w i = 1 → ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (Finset.affineCombination k s p₁) w -ᵥ p₂
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_inter_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α},
  Set.Ioo a₁ b₁ ∩ Set.Ioo a₂ b₂ = Set.Ioo (max a₁ a₂) (min b₁ b₂)
-- Mathlib.Topology.UnitInterval
unitInterval.continuous_symm : Continuous unitInterval.symm
-- Mathlib.Data.Prod.Basic
Prod.forall' : ∀ {α : Type u_1} {β : Type u_2} {p : α → β → Prop}, (∀ (x : α × β), p x.1 x.2) ↔ ∀ (a : α) (b : β), p a b
-- Mathlib.Data.Sym.Sym2
Sym2.diagElem_mk : ∀ {α : Type u_1} {a b : α} (h : s(a, b).IsDiag), s(a, b).diagElem h = a
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.topDownAnalyze : Lean.Expr → Lean.MetaM Lean.PrettyPrinter.Delaborator.OptionsPerPos
-- Mathlib.Topology.Category.Stonean.Limits
Stonean.extremallyDisconnected_pullback : ∀ {X Y Z : Stonean} {f : X ⟶ Z} (i : Y ⟶ Z),
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) →
    ExtremallyDisconnected
      ↑{xy | (CategoryTheory.ConcreteCategory.hom f) xy.1 = (CategoryTheory.ConcreteCategory.hom i) xy.2}
-- Mathlib.Analysis.Convex.Function
/-- Left translation preserves strict concavity.  -/
StrictConcaveOn.translate_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCancelCommMonoid E] [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E]
  [inst_6 : SMul 𝕜 β] {s : Set E} {f : E → β},
  StrictConcaveOn 𝕜 s f → ∀ (c : E), StrictConcaveOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_union : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF), (m₁.union m₂ ⋯ ⋯).isEmpty = (m₁.isEmpty && m₂.isEmpty)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct
SSet.instInnerFibrationMapIhom : ∀ {E B X : SSet} (p : E ⟶ B) [SSet.InnerFibration p], SSet.InnerFibration ((CategoryTheory.ihom X).map p)
-- Lean.Elab.Tactic.Conv.Pattern
Lean.Elab.Tactic.Conv.PatternMatchState.all.injEq : ∀ (subgoals subgoals_1 : Array Lean.MVarId),
  (Lean.Elab.Tactic.Conv.PatternMatchState.all subgoals = Lean.Elab.Tactic.Conv.PatternMatchState.all subgoals_1) =
    (subgoals = subgoals_1)
-- Mathlib.Algebra.Lie.Ideal
LieHom.ker_toSubmodule : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L'), ↑f.ker = (↑f).ker
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.algebraMap_residue_eq_residue_algebraMap : ∀ {K : outParam (Type u_5)} {L : outParam (Type u_6)} {Γ₀ : outParam (Type u_7)} {Γ₁ : outParam (Type u_8)}
  [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_4 : LinearOrderedCommGroupWithZero Γ₁] (vK : Valuation K Γ₀) (vL : Valuation L Γ₁) [inst_5 : vK.HasExtension vL]
  (x : ↥vK.valuationSubring),
  (algebraMap (IsLocalRing.ResidueField ↥vK.valuationSubring) (IsLocalRing.ResidueField ↥vL.valuationSubring))
      ((IsLocalRing.residue ↥vK.valuationSubring) x) =
    (IsLocalRing.residue ↥vL.valuationSubring) ((algebraMap ↥vK.valuationSubring ↥vL.valuationSubring) x)