mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Basic
/-- The first list is a suffix of the second.

`IsSuffix l₁ l₂`, written `l₁ <:+ l₂`, means that there exists some `t : List α` such that `l₂` has
the form `t ++ l₁`.

The function `List.isSuffixOf` is a Boolean equivalent.


Conventions for notations in identifiers:

 * The recommended spelling of `<:+` in identifiers is `suffix` (not `isSuffix`). -/
List.«term_<:+_» : Lean.TrailingParserDescr
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.instSliceableListSliceNat.match_1.eq_1 : ∀ (motive : Option ℕ → Sort u_1) (h_1 : Unit → motive none) (h_2 : (stop : ℕ) → motive (some stop)),
  (match none with
    | none => h_1 ()
    | some stop => h_2 stop) =
    h_1 ()
-- Mathlib.ModelTheory.Definability
Set.Definable.himp : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {s t : Set (α → M)},
  A.Definable L s → A.Definable L t → A.Definable L (s ⇨ t)
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.polar_eq_iInter : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {s : Set E},
  B.polar s = ⋂ x ∈ s, {y | ‖(B x) y‖ ≤ 1}
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instNonAssocSemiringOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : NonAssocSemiring Mᵃᵒᵖ], DomAddAct.instNonAssocSemiringOfAddOpposite = inst
-- Mathlib.RingTheory.Coalgebra.Basic
Prod.comul_comp_snd : ∀ (R : Type u) (A : Type v) (B : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : AddCommMonoid B]
  [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : Coalgebra R A] [inst_6 : Coalgebra R B],
  CoalgebraStruct.comul ∘ₗ LinearMap.snd R A B =
    TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ CoalgebraStruct.comul
-- Mathlib.Topology.Order.Real
ENNReal.instT2Space : T2Space ENNReal
-- Mathlib.Algebra.Order.Sub.Prod
Pi.orderedSub : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → Preorder (α i)] [inst_1 : (i : ι) → Add (α i)]
  [inst_2 : (i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)], OrderedSub ((i : ι) → α i)
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.sectR_map₂ : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] (b : B) (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b_1 : C} {f g : a ⟶ b_1} (a_1 : f ⟶ g),
  (CategoryTheory.Bicategory.Prod.sectR b C).map₂ a_1 =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id b)) a_1
-- Qq.Macro
Qq.Impl.isAssignablePattern : Lean.Expr → Lean.MetaM Bool
-- Lean.Data.PersistentArray
Lean.Array.toPArray' : {α : Type u} → Array α → Lean.PersistentArray α
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- The `enorm` of a strongly measurable function is measurable.

Unlike `StrongMeasurable.norm` and `StronglyMeasurable.nnnorm`, this lemma proves measurability,
**not** strong measurability. This is an intentional decision: for functions taking values in
ℝ≥0∞, measurability is much more useful than strong measurability.  -/
MeasureTheory.StronglyMeasurable.enorm : ∀ {α : Type u_1} {x : MeasurableSpace α} {ε : Type u_5} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  {f : α → ε}, MeasureTheory.StronglyMeasurable f → Measurable fun x => ‖f x‖ₑ
-- Lean.Parser.Types
Lean.Parser.ParserState.stxStack : Lean.Parser.ParserState → Lean.Parser.SyntaxStack
-- Lean.Attributes
Lean.AttributeImplBuilder : Type
-- Init.Data.Array.Lemmas
Array.filterMap_eq_map : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {as : Array α} {f : α → β},
  stop = as.size → Array.filterMap (some ∘ f) as 0 stop = Array.map f as
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.parallelFamily_obj_zero : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)),
  (CategoryTheory.Limits.parallelFamily f).obj CategoryTheory.Limits.WalkingParallelFamily.zero = X
-- Init.Data.UInt.Basic
instAndOpUSize : AndOp USize
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.WideSubcategory.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : P.IsMultiplicative] {X Y : CategoryTheory.WideSubcategory P} {f g : X ⟶ Y}, f.hom = g.hom → f = g
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₂ → (t₁ ∩ t₂).getD k fallback = fallback
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSucc_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j),
  (CategoryTheory.SmallObject.SuccStruct.extendToSucc hj F τ).map (CategoryTheory.homOfLE hi) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso hj F τ i₁ ⋯).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE hi))
        (CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso hj F τ i₂ hi₂).inv)
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_intCast_mul : ∀ {S : Type v} [inst : Ring S] {p : Polynomial S} {a : ℤ} {k : ℕ}, (↑a * p).coeff k = ↑a * p.coeff k
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_σ₀Iter : ∀ (i : ℕ) {n m : ℕ} (hi : autoParam (n + i = m) SimplexCategory.δ₀Iter_σ₀Iter._auto_1),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter i hi) (SimplexCategory.σ₀Iter i hi) =
    CategoryTheory.CategoryStruct.id { len := n }
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.closedBall_eq_univ_of_half_period_le : ∀ (p : ℝ), p ≠ 0 → ∀ (x : AddCircle p) {ε : ℝ}, |p| / 2 ≤ ε → Metric.closedBall x ε = Set.univ
-- Mathlib.Topology.Algebra.Ring.Basic
Subring.instIsTopologicalRing : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Ring R] [IsTopologicalRing R] (S : Subring R),
  IsTopologicalRing ↥S
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift.eq_1 : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (H' :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)),
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift f g H' =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pullback.snd f g))
      (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.evaln.eq_7 : ∀ (k : ℕ) (cf cg : Nat.Partrec.Code),
  Nat.Partrec.Code.evaln k.succ (cf.comp cg) = fun n => do
    guard (n ≤ k)
    let x ← Nat.Partrec.Code.evaln (k + 1) cg n
    Nat.Partrec.Code.evaln (k + 1) cf x
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.u_smooth : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E],
  ContDiff ℝ (↑⊤) ExistsContDiffBumpBase.u
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.ordCompare_maxKey!_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap α (fun x => β) compare}
  [inst_2 : Inhabited α] {k : α} {f : β → β}, compare (Std.DTreeMap.Const.modify t k f).maxKey! t.maxKey! = Ordering.eq
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_toNat_le_self`. -/
ENat.coe_toNat_le_self : ∀ (n : ℕ∞), ↑n.toNat ≤ n
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The isomorphism `(K.truncGE' e).X i ≅ K.X i'` when `e.f i = i'`
and `e.BoundaryGE i` does not hold.  -/
HomologicalComplex.truncGE'XIso : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncGE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      {i : ι} → {i' : ι'} → e.f i = i' → ¬e.BoundaryGE i → ((K.truncGE' e).X i ≅ K.X i')
-- Mathlib.Data.Complex.Basic
Complex.normSq_ofReal : ∀ (r : ℝ), Complex.normSq ↑r = r * r
-- Mathlib.Order.Partition.Finpartition
Finpartition.restrict.eq_1 : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] {a b : α} (P : Finpartition a)
  (hb : b ≤ a),
  P.restrict hb =
    { parts := (Finset.image (fun x => x ⊓ b) P.parts).erase ⊥, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → γ a} {k : α} [inst_1 : Inhabited (γ k)],
  t.WF → (Std.DTreeMap.Internal.Impl.map f t).get! k = (Option.map (f k) (t.get? k)).get!
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.op_whiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor D E} (α : F ⟶ G),
  CategoryTheory.NatTrans.op (CategoryTheory.Functor.whiskerRight α H) =
    CategoryTheory.CategoryStruct.comp (G.opComp H).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op α) H.op)
        (F.opComp H).inv)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.instFinite : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [Finite R],
  Finite (Matrix.SpecialLinearGroup n R)
-- Init.Data.Nat.Lemmas
Nat.mul_self_le_mul_self : ∀ {m n : ℕ}, m ≤ n → m * m ≤ n * n
-- Mathlib.Data.Set.Card
Set.ncard_inter_add_ncard_sdiff_eq_ncard : ∀ {α : Type u_1} (s t : Set α),
  autoParam s.Finite Set.ncard_inter_add_ncard_sdiff_eq_ncard._auto_1 → (s ∩ t).ncard + (s \ t).ncard = s.ncard
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_lt_top : ∀ {a b : ENNReal}, a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.eq_zero_or_one_of_isField : ∀ {R₁ : Type u_3} {K : Type u_4} [inst : CommRing R₁] [inst_1 : Field K] [inst_2 : Algebra R₁ K] [IsFractionRing R₁ K],
  IsField R₁ → ∀ (I : FractionalIdeal (nonZeroDivisors R₁) K), I = 0 ∨ I = 1
-- Mathlib.Analysis.Normed.Module.Basic
/-- This is a simpler version of `norm_algebraMap` when `‖1‖ = 1` in `𝕜'`.  -/
norm_algebraMap' : ∀ {𝕜 : Type u_1} (𝕜' : Type u_2) [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜']
  [NormOneClass 𝕜'] (x : 𝕜), ‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.toList_rii : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.toList_rii._auto_1)
  {t : Std.DTreeMap.Raw α β cmp}, Std.Slice.toList (Std.Rii.Sliceable.mkSlice t *...*) = t.toList
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_map_prod : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {B : Type u_2} [inst_10 : PartialOrder B]
  [inst_11 : Ring B] [inst_12 : StarRing B] [inst_13 : TopologicalSpace B] [inst_14 : StarOrderedRing B]
  [inst_15 : Algebra ℝ B] [inst_16 : ContinuousFunctionalCalculus ℝ B IsSelfAdjoint]
  [inst_17 : ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint] [IsSemitopologicalRing B] [T2Space B]
  [inst_20 : StarOrderedRing (A × B)] [inst_21 : NonnegSpectrumClass ℝ B] [inst_22 : NonnegSpectrumClass ℝ (A × B)]
  {a : A} {b : B} {x : ℝ},
  IsUnit a →
    IsUnit b →
      autoParam (0 ≤ a) CFC.rpow_map_prod._auto_1 →
        autoParam (0 ≤ b) CFC.rpow_map_prod._auto_3 → CFC.rpow (a, b) x = (a ^ x, b ^ x)
-- Lean.Meta.Closure
Lean.Meta.Closure.mkForall : Array Lean.LocalDecl → Lean.Expr → Lean.Expr
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of a tuple does not change under scaling.  -/
Height.mulHeight_smul_eq_mulHeight : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) {c : K},
  c ≠ 0 → Height.mulHeight (c • x) = Height.mulHeight x
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Valuation.mk.congr_simp : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : LinearOrderedCommMonoidWithZero Γ₀] [inst_1 : Ring R]
  (toMonoidWithZeroHom toMonoidWithZeroHom_1 : R →*₀ Γ₀)
  (e_toMonoidWithZeroHom : toMonoidWithZeroHom = toMonoidWithZeroHom_1)
  (map_add_le_max' :
    ∀ (x y : R),
      (↑toMonoidWithZeroHom).toFun (x + y) ≤ max ((↑toMonoidWithZeroHom).toFun x) ((↑toMonoidWithZeroHom).toFun y)),
  { toMonoidWithZeroHom := toMonoidWithZeroHom, map_add_le_max' := map_add_le_max' } =
    { toMonoidWithZeroHom := toMonoidWithZeroHom_1, map_add_le_max' := ⋯ }
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.equivOfInverse'_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁)
  (h₁ : f₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂) (h₂ : f₂ ∘SL f₁ = ContinuousLinearMap.id R₁ M₁) (x : M₁),
  (ContinuousLinearEquiv.equivOfInverse' f₁ f₂ h₁ h₂) x = f₁ x
-- Mathlib.CategoryTheory.Grothendieck
/-- The underlying object in `C`  -/
CategoryTheory.Grothendieck.base : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} → CategoryTheory.Grothendieck F → C
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.instIsCardinalForSmallObjectArgumentJAleph0 : SSet.modelCategoryQuillen.J.IsCardinalForSmallObjectArgument Cardinal.aleph0
-- Mathlib.Order.UpperLower.Principal
UpperSet.map_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (a : α),
  (UpperSet.map f) (UpperSet.Ici a) = UpperSet.Ici (f a)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraComplex.ofComplex_comp_toComplex : CliffordAlgebraComplex.ofComplex.comp CliffordAlgebraComplex.toComplex =
  AlgHom.id ℝ (CliffordAlgebra CliffordAlgebraComplex.Q)
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Erase matches containing the hypothesis `h` from `ms`.  -/
Aesop.ForwardRuleMatches.eraseHyp : Lean.FVarId → Aesop.ForwardRuleMatches → Aesop.ForwardRuleMatches
-- Std.Http.Transport
/-- Client to server direction.
 -/
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.SharedState.clientToServer : Std.Http.Internal.Mock.SharedState✝ → Std.CloseableChannel ByteArray
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_restrictScalars : ∀ (K : Type u_1) {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] [inst_5 : Algebra L' L] [inst_6 : IsScalarTower K L' L]
  {E : IntermediateField L' L}, ↑(IntermediateField.restrictScalars K E) = ↑E
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- If `Φ : SuccStruct C` and `f` is a morphism in `C` which
satisfies `Φ.prop f`, then this is the isomorphism of arrows
between `f` and `Φ.toSuccArrow X`.  -/
CategoryTheory.SmallObject.SuccStruct.prop.arrowIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Φ : CategoryTheory.SmallObject.SuccStruct C} →
      {X Y : C} → {f : X ⟶ Y} → Φ.prop f → (CategoryTheory.Arrow.mk f ≅ Φ.toSuccArrow X)
-- Lean.Data.LOption
Lean.LOption.some : {α : Type u} → α → Lean.LOption α
-- Init.Data.List.Find
List.findSome?_eq_some_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} {b : β},
  List.findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ x ∈ l₁, f x = none
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_mul : ∀ (a b : BitVec 64), { toBitVec := a * b } = { toBitVec := a } * { toBitVec := b }
-- Mathlib.Analysis.Convex.Gauge
gauge_lt_of_mem_smul : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
  [ContinuousSMul ℝ E] (x : E) (ε : ℝ), 0 < ε → IsOpen s → x ∈ ε • s → gauge s x < ε
-- Mathlib.Tactic.ContinuousFunctionalCalculus
/-- A tactic used to automatically discharge goals relating to the continuous functional calculus,
specifically concerning continuity of the functions involved.  -/
cfcContTac : Lean.ParserDescr
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.map_tmul : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C] [inst_13 : Semiring D]
  [inst_14 : Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D) (a : A) (b : B),
  (Algebra.TensorProduct.map f g) (a ⊗ₜ[R] b) = f a ⊗ₜ[R] g b
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instAdd : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → [Add A] → Add (CStarMatrix m n A)
-- Mathlib.GroupTheory.ArchimedeanDensely
not_denselyOrdered_withZero_int : ¬DenselyOrdered (WithZero (Multiplicative ℤ))
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- `BilinForm.toMatrix b` is the equivalence between `R`-bilinear forms on `M` and
`n`-by-`n` matrices with entries in `R`, if `b` is an `R`-basis for `M`.  -/
Matrix.toBilin : {R₁ : Type u_1} →
  {M₁ : Type u_2} →
    [inst : CommSemiring R₁] →
      [inst_1 : AddCommMonoid M₁] →
        [inst_2 : Module R₁ M₁] →
          {n : Type u_5} →
            [Fintype n] → [DecidableEq n] → Module.Basis n R₁ M₁ → Matrix n n R₁ ≃ₗ[R₁] LinearMap.BilinForm R₁ M₁
-- Mathlib.Order.Preorder.Finsupp
Finsupp.coe_lt_coe : ∀ {ι : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : Preorder M] {f g : ι →₀ M}, ⇑f < ⇑g ↔ f < g
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
ContinuousLinearMap.aestronglyMeasurable_comp₂ : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_4} [inst : NontriviallyNormedField 𝕜]
  {E : Type u_5} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_6}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_7} [inst_5 : NormedAddCommGroup G]
  [inst_6 : NormedSpace 𝕜 G] (L : E →L[𝕜] F →L[𝕜] G) {f : α → E} {g : α → F},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun x => (L (f x)) (g x)) μ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItem.tags? : Lean.Lsp.ResolvableCompletionItem → Option (Array Lean.Lsp.CompletionItemTag)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.toProd.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  Monoid.Coprod.toProd = Monoid.Coprod.lift (MonoidHom.inl M N) (MonoidHom.inr M N)
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.fiberProdLex : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set (Lex (α × β))},
  s.IsPWO → ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_mono : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] {s t : Set α},
  s ⊆ t → (Ordinal.type fun x1 x2 => x1 < x2) ≤ Ordinal.type fun x1 x2 => x1 < x2
-- Mathlib.Topology.ClusterPt
isClosed_iff_forall_filter : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsClosed s ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ Filter.principal s → F ≤ nhds x → x ∈ s
-- Mathlib.Order.Interval.Finset.Defs
/-- This mixin class describes an order where all intervals bounded above are finite. This is
slightly weaker than `LocallyFiniteOrder` + `OrderBot` as it allows empty types.  -/
LocallyFiniteOrderBot : (α : Type u_1) → [Preorder α] → Type u_1
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
/-- Every left pre-Lie algebra is a right pre-Lie algebra with the opposite multiplication  -/
RightPreLieAlgebra.instLeftPreLieAlgebraMulOpposite : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] → [inst_1 : RightPreLieRing L] → [RightPreLieAlgebra R L] → LeftPreLieAlgebra R Lᵐᵒᵖ
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.isHashSelf_mapₘ : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] [ReflBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → δ a},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.IsHashSelf (↑(m.mapₘ f)).buckets
-- Mathlib.CategoryTheory.Sites.Sheafification
/-- Given a sheaf `Q` and a morphism `P ⟶ Q`, construct a morphism from `sheafify J P` to `Q`.  -/
CategoryTheory.sheafifyLift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_2 : CategoryTheory.HasWeakSheafify J D] →
            {P Q : CategoryTheory.Functor Cᵒᵖ D} →
              (P ⟶ Q) → CategoryTheory.Presheaf.IsSheaf J Q → (CategoryTheory.sheafify J P ⟶ Q)
-- Mathlib.NumberTheory.Height.NumberField
/-- The infinite places of a number field `K` as a `Multiset` of absolute values on `K`,
with multiplicity given by `InfinitePlace.mult`.  -/
NumberField.multisetInfinitePlace : (K : Type u_1) → [inst : Field K] → [NumberField K] → Multiset (AbsoluteValue K ℝ)
-- Init.Data.Nat.Lemmas
Nat.log2_eq_iff : ∀ {n k : ℕ}, n ≠ 0 → (n.log2 = k ↔ 2 ^ k ≤ n ∧ n < 2 ^ (k + 1))
-- Lean.Compiler.LCNF.Basic
/-- The name of the declaration from the `Environment` it came from
 -/
Lean.Compiler.LCNF.Signature.name : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Signature pu → Lean.Name
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.push.inj : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {k : K} {a : σ → Γ k} {a_1 : Turing.TM2.Stmt Γ Λ σ}
  {k_1 : K} {a_2 : σ → Γ k_1} {a_3 : Turing.TM2.Stmt Γ Λ σ},
  Turing.TM2.Stmt.push k a a_1 = Turing.TM2.Stmt.push k_1 a_2 a_3 → k = k_1 ∧ a ≍ a_2 ∧ a_1 = a_3
-- Mathlib.CategoryTheory.Sites.LocalSite
CategoryTheory.GrothendieckTopology.IsLocalSite.toPresheafFiber_pointPresheafFiberIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_2 : J.IsLocalSite] {A : Type u'}
  [inst_3 : CategoryTheory.Category.{v', u'} A] [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  {P : CategoryTheory.Functor Cᵒᵖ A} (X : C)
  (x : (CategoryTheory.GrothendieckTopology.IsLocalSite.point J).fiber.obj X),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.IsLocalSite.point J).toPresheafFiber X x P)
      (CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso J P).hom =
    P.map (CategoryTheory.shrinkCoyonedaObjObjEquiv x).op
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tdiv_add_tmod : ∀ (a b : ℤ), b * a.tdiv b + a.tmod b = a
-- Mathlib.CategoryTheory.Simple
/-- A subobject is simple iff it is an atom in the subobject lattice.  -/
CategoryTheory.subobject_simple_iff_isAtom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} (Y : CategoryTheory.Subobject X),
  CategoryTheory.Simple (CategoryTheory.Subobject.underlying.obj Y) ↔ IsAtom Y