mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
/-- Given two object properties `P` and `Q`, the property of morphisms whose source
satisfies `P` and target satisfies `Q`.  -/
CategoryTheory.MorphismProperty.ofObjectProperty : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C → CategoryTheory.MorphismProperty C
-- Init.Notation
/-- The `seal foo` command ensures that the definition of `foo` is sealed, meaning it is marked as `[irreducible]`.
This command is particularly useful in contexts where you want to prevent the reduction of `foo` in proofs.

In terms of functionality, `seal foo` is equivalent to `attribute [local irreducible] foo`.
This attribute specifies that `foo` should be treated as irreducible only within the local scope,
which helps in maintaining the desired abstraction level without affecting global settings.
 -/
Lean.Parser.commandSeal__ : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.trans_refl : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), e.trans (LinearIsometryEquiv.refl R₂ E₂) = e
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbvDef : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {b : NNReal} (hb : 1 < b), IsNonarchimedean (v.intAdicAbvDef hb)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
_private.Std.Tactic.BVDecide.LRAT.Internal.Clause.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.isUnit.match_1.eq_2 : ∀ {n : ℕ} (motive : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (x : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (h_1 : (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → motive [l])
  (h_2 : (x : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → motive x),
  (∀ (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)), x = [l] → False) →
    (match x with
      | [l] => h_1 l
      | x => h_2 x) =
      h_2 x
-- Init.Data.Array.Zip
Array.zipWith_foldl_eq_zip_foldl : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {as : Array α} {bs : Array β} {g : δ → γ → δ}
  {f : α → β → γ} {i : δ},
  Array.foldl g i (Array.zipWith f as bs) = Array.foldl (fun r p => g r (f p.1 p.2)) i (as.zip bs)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf.eq_1 : ∀ {R : Type u_1} [inst : ConditionallyCompleteLattice R] [inst_1 : Div R] [inst_2 : NatCast R] (u : ℕ → R),
  LinearGrowth.linearGrowthInf u = Filter.liminf (fun n => u n / ↑n) Filter.atTop
-- Mathlib.Data.Nat.Cast.Order.Field
Nat.one_div_lt_one_div : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {n m : ℕ},
  n < m → 1 / (↑m + 1) < 1 / (↑n + 1)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_sum_lt : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {ι : Type u_7} {s : Finset ι} {f : ι → R} {g : Γ₀}, g ≠ 0 → (∀ i ∈ s, v (f i) < g) → v (∑ i ∈ s, f i) < g
-- Batteries.Data.Vector.Lemmas
Vector.finIdxOf?_eq_none_iff : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [LawfulBEq α] {v : Vector α n} {a : α}, v.finIdxOf? a = none ↔ a ∉ v
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.FindSplitImpl.Context.exceptionSet : Lean.Meta.FindSplitImpl.Context → Lean.ExprSet
-- Mathlib.Analysis.SpecialFunctions.Exp
Complex.tendsto_exp_comap_re_atBot_nhdsNE : Filter.Tendsto Complex.exp (Filter.comap Complex.re Filter.atBot) (nhdsWithin 0 {0}ᶜ)
-- Std.Sync.CancellationContext
/-- Recursively cancels a context and all its children with the given reason.
 -/
_private.Std.Sync.CancellationContext.0.Std.CancellationContext.cancelChildren : Std.CancellationContext.State → UInt64 → Std.CancellationReason → BaseIO Std.CancellationContext.State
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
SSet.finite_iSup_iff : ∀ {X : SSet} {ι : Type u_1} [Finite ι] (A : ι → X.Subcomplex), (⨆ i, A i).toSSet.Finite ↔ ∀ (i : ι), (A i).toSSet.Finite
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Meromorphic functions have normal form outside of a discrete subset in the domain of
meromorphicity.  -/
MeromorphicOn.meromorphicNFAt_mem_codiscreteWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U → {x | MeromorphicNFAt f x} ∈ Filter.codiscreteWithin U
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.PEquivOn.restrict_equiv : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [inst : LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i}
  [inst_1 : SuccOrder ι] {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s t : Set ι}
  (e : InverseSystem.PEquivOn f equivSucc t) (h : s ⊆ t) (i : ↑s), (e.restrict h).equiv i = e.equiv ⟨↑i, ⋯⟩
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edgeSet_top : ∀ {V : Type u} {G : SimpleGraph V}, ⊤.edgeSet = G.edgeSet
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.instSmoothOfIsStandardSmooth : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsStandardSmooth R S], Algebra.Smooth R S
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- If a function is differentiable on open sets `s i`, it is differentiable on their union.  -/
DifferentiableOn.iUnion_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {ι : Type u_4} {s : ι → Set E},
  (∀ (i : ι), DifferentiableOn 𝕜 f (s i)) → (∀ (i : ι), IsOpen (s i)) → DifferentiableOn 𝕜 f (⋃ i, s i)
-- Mathlib.CategoryTheory.IsConnected
/-- A zigzag in a discrete category entails an equality of its extremities  -/
CategoryTheory.eq_of_zigzag : ∀ (X : Type u_1) {a b : CategoryTheory.Discrete X}, CategoryTheory.Zigzag a b → a.as = b.as
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
/-- The base change of a quadratic form.  -/
QuadraticForm.baseChange : {R : Type uR} →
  (A : Type uA) →
    {M₂ : Type uM₂} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module R M₂] → [Invertible 2] → QuadraticForm R M₂ → QuadraticForm A (TensorProduct R A M₂)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a localization map `f : M →* N`, a section function sending `z : N` to some
`(x, y) : M × S` such that `f x * (f y)⁻¹ = z`.  -/
Submonoid.LocalizationMap.sec : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} → {N : Type u_2} → [inst_1 : CommMonoid N] → S.LocalizationMap N → N → M × ↥S
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.IsClosedUnderSubobjects.prop_of_mono : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C}
  [self : P.IsClosedUnderSubobjects] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f], P Y → P X
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.CanonicallyOverClass.over_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : C)
  [inst_1 : CategoryTheory.CanonicallyOverClass X Y] [inst_2 : CategoryTheory.OverClass Y S],
  X ↘ S = CategoryTheory.CategoryStruct.comp (X ↘ Y) (Y ↘ S)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.mk : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : Algebra R A] →
                  [inst_6 : Algebra R B] →
                    (toAlgEquiv : A ≃ₐ[R] B) →
                      autoParam (Continuous toAlgEquiv.toFun) Homeomorph.continuous_toFun._autoParam →
                        autoParam (Continuous toAlgEquiv.invFun) Homeomorph.continuous_invFun._autoParam → A ≃A[R] B
-- Lean.Environment
_private.Lean.Environment.0.Lean.Kernel.Environment.isQuotInit : Lean.Kernel.Environment → Bool
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.ofAlgEquiv_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : Ring T] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T),
  (h.ofAlgEquiv e).root = e h.root
-- Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate
implicitFunctionOfBivariate.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : IsRCLikeNormedField 𝕜] {E₁ : Type u_2}
  [inst_2 : NormedAddCommGroup E₁] [inst_3 : NormedSpace 𝕜 E₁] [inst_4 : CompleteSpace E₁] {E₂ : Type u_3}
  [inst_5 : NormedAddCommGroup E₂] [inst_6 : NormedSpace 𝕜 E₂] [inst_7 : CompleteSpace E₂] {F : Type u_4}
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : CompleteSpace F] {u u_1 : E₁ × E₂}
  (e_u : u = u_1) {f f_1 : E₁ → E₂ → F} (e_f : f = f_1) {f₁ f₁_1 : E₁ → E₂ → E₁ →L[𝕜] F} (e_f₁ : f₁ = f₁_1)
  {f₂ f₂_1 : E₁ → E₂ → E₂ →L[𝕜] F} (e_f₂ : f₂ = f₂_1)
  (df₁ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f x v.2) (f₁ v.1 v.2) v.1)
  (df₂ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f v.1 x) (f₂ v.1 v.2) v.2) (cf₁ : ContinuousAt (↿f₁) u)
  (cf₂ : ContinuousAt (↿f₂) u) (if₂u : (f₂ u.1 u.2).IsInvertible) (a a_1 : E₁),
  a = a_1 → implicitFunctionOfBivariate df₁ df₂ cf₁ cf₂ if₂u a = implicitFunctionOfBivariate ⋯ ⋯ ⋯ ⋯ ⋯ a_1
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.State.mk.sizeOf_spec : ∀ (share : Lean.Meta.Sym.AlphaShareCommon.State) (maxFVar : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.FVarId))
  (proofInstInfo : Lean.PHashMap Lean.Name (Option Lean.Meta.Sym.ProofInstInfo))
  (inferType : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr)
  (getLevel : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Level)
  (congrInfo : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.CongrInfo)
  (defEqI : Lean.PHashMap (Lean.Meta.Sym.ExprPtr × Lean.Meta.Sym.ExprPtr) Bool)
  (extensions : Array Lean.Meta.Sym.SymExtensionState) (issues : List Lean.MessageData)
  (canon : Lean.Meta.Sym.Canon.State) (instanceOverrides : Lean.PHashMap Lean.Expr Lean.Expr) (debug : Bool),
  sizeOf
      { share := share, maxFVar := maxFVar, proofInstInfo := proofInstInfo, inferType := inferType,
        getLevel := getLevel, congrInfo := congrInfo, defEqI := defEqI, extensions := extensions, issues := issues,
        canon := canon, instanceOverrides := instanceOverrides, debug := debug } =
    1 + sizeOf share + sizeOf maxFVar + sizeOf proofInstInfo + sizeOf inferType + sizeOf getLevel + sizeOf congrInfo +
                sizeOf defEqI +
              sizeOf extensions +
            sizeOf issues +
          sizeOf canon +
        sizeOf instanceOverrides +
      sizeOf debug
-- Mathlib.SetTheory.ZFC.VonNeumann
/-- Every set is in some element of the von Neumann hierarchy.  -/
ZFSet.exists_mem_vonNeumann : ∀ (x : ZFSet.{u_1}), ∃ o, x ∈ ZFSet.vonNeumann o
-- Mathlib.Topology.Algebra.Affine
ContinuousOn.lineMap : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : AddCommGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] [inst_5 : Ring R]
  [inst_6 : Module R V] [inst_7 : TopologicalSpace R] [ContinuousSMul R V] {X : Type u_6} [inst_9 : TopologicalSpace X]
  {f₁ f₂ : X → P} {g : X → R} {s : Set X},
  ContinuousOn f₁ s →
    ContinuousOn f₂ s → ContinuousOn g s → ContinuousOn (fun x => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) s
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.continuous_expMapBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Continuous ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSets_iff : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} (π : ι → Set (Set Ω)) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.iIndepSets π μ ↔
    ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ π i) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dCokernelSequence_g : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_5),
  (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃).g =
    X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k fallback : α},
  k ∈ m → (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
/-- A root pairing is said to be crystallographic if the pairing between a root and coroot is
always an integer.  -/
RootPairing.IsCrystallographic : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → Prop
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- Any group is isomorphic to the units of itself adjoined with `0`.  -/
WithZero.unitsWithZeroEquiv : {α : Type u_1} → [inst : Group α] → (WithZero α)ˣ ≃* α
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arctan`, version subtracting vectors.  -/
Orientation.oangle_sub_left_eq_arctan_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  o.oangle x y = ↑(Real.pi / 2) → o.oangle (x - y) x = ↑(Real.arctan (‖y‖ / ‖x‖))
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_bot_iff : ∀ {α : Type u_1} {s : Set α}, ⊥.IsClique s ↔ s.Subsingleton
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.List.filterM.eq_1 : ∀ {m : Type → Type v} [inst : Monad m] {α : Type} (p : α → m Bool) (as : List α),
  List.filterM p as = do
    let as ← List.filterAuxM p as []
    pure as.reverse
-- Std.Data.Iterators.Consumers.Monadic.Set
/-- Traverses the given iterator and stores the emitted values in a `HashSet`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.toHashSet`.
 -/
Std.IterM.Total.toHashSet : {α β : Type w} →
  [inst : BEq β] →
    [inst_1 : Hashable β] →
      {m : Type w → Type w'} →
        [Monad m] →
          [inst_3 : Std.Iterator α m β] →
            [Std.Iterators.Finite α m] → [Std.IteratorLoop α m m] → Std.IterM.Total m β → m (Std.HashSet β)
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.cg_bot : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M], ⊥.CG
-- Mathlib.Algebra.Group.Int.Defs
Int.instMonoid : Monoid ℤ
-- Std.Data.TreeSet.Basic
/-- Checks whether an element is present in a set and inserts the element if it was not found.
If the tree set already contains an element that is equal (with regard to `cmp` to the given
element, then the tree set is returned unchanged.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.TreeSet.containsThenInsert : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → Bool × Std.TreeSet α cmp
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.instReflBEqPolyCnstr : ReflBEq Nat.Internal.Linear.PolyCnstr
-- Init.Data.List.Basic
List.Lex.below.nil : ∀ {α : Type u} {r : α → α → Prop} {motive : (as bs : List α) → List.Lex r as bs → Prop} {a : α} {l : List α},
  List.Lex.below ⋯
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDerivWithin_smul_const_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {x : E} {A : Type u_4} [inst_5 : NormedRing A] [inst_6 : NormedAlgebra 𝕜 A] [inst_7 : Module A F]
  [inst_8 : IsScalarTower 𝕜 A F] [inst_9 : IsBoundedSMul A F] {i : ℕ} {v : F} {f : E → A},
  ContDiffWithinAt 𝕜 (↑i) f s x →
    UniqueDiffOn 𝕜 s →
      x ∈ s →
        iteratedFDerivWithin 𝕜 i (fun y => f y • v) s x =
          ((ContinuousLinearMap.id 𝕜 A).smulRight v).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.addLinearEquiv_apply' : ∀ {m n : ℕ} {R : Type u_2} [inst : Ring R] (f : ↥(Polynomial.degreeLT R (m + n))),
  ↑((Polynomial.degreeLT.addLinearEquiv R m n) f).1 = ↑f %ₘ Polynomial.X ^ m ∧
    ↑((Polynomial.degreeLT.addLinearEquiv R m n) f).2 = ↑f /ₘ Polynomial.X ^ m
-- Mathlib.Algebra.GCDMonoid.Basic
StrongNormalizedGCDMonoid.mk : {α : Type u_2} →
  [inst : CommMonoidWithZero α] →
    [toStrongNormalizationMonoid : StrongNormalizationMonoid α] →
      [toGCDMonoid : GCDMonoid α] →
        (∀ (a b : α), normalize (gcd a b) = gcd a b) →
          (∀ (a b : α), normalize (lcm a b) = lcm a b) → StrongNormalizedGCDMonoid α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq₂ : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  W.Equation x₁ y₁ →
    W.Equation x₂ y₂ →
      ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) →
        WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x₂ (Polynomial.C y₂) =
          WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x₂
            (WeierstrassCurve.Affine.linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
-- Init.Data.UInt.Bitwise
USize.toUInt8_or : ∀ (a b : USize), (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Functor.constCompEvaluationObj_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C) (X_1 : D),
  (CategoryTheory.Functor.constCompEvaluationObj D X).hom.app X_1 = CategoryTheory.CategoryStruct.id X_1
-- Mathlib.Algebra.Lie.Killing
LieAlgebra.IsKilling.isLieAbelian_iff_subsingleton : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsKilling R L] [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R],
  IsLieAbelian L ↔ Subsingleton L
-- Mathlib.LinearAlgebra.Isomorphisms
/-- Corollary of the third isomorphism theorem: `[S : T] [M : S] = [M : T]`  -/
Submodule.card_quotient_mul_card_quotient : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S T : Submodule R M),
  T ≤ S → Nat.card ↥(Submodule.map T.mkQ S) * Nat.card (M ⧸ S) = Nat.card (M ⧸ T)
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.ofPermHomFun_apply_mem_support_cycle_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)) {x : α} {c : ↥g.cycleFactorsFinset},
  a.ofPermHomFun τ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to0.trAux.match_1.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → σ → Sort u_4) (d : Turing.Dir)
  (q : Turing.TM1.Stmt Γ Λ σ) (v : σ)
  (h_1 : (d : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.move d q) v)
  (h_2 : (a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.write a q) v)
  (h_3 : (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.load a q) v)
  (h_4 : (p : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.branch p q₁ q₂) v)
  (h_5 : (l : Γ → σ → Λ) → (v : σ) → motive (Turing.TM1.Stmt.goto l) v) (h_6 : (v : σ) → motive Turing.TM1.Stmt.halt v),
  (match Turing.TM1.Stmt.move d q, v with
    | Turing.TM1.Stmt.move d q, v => h_1 d q v
    | Turing.TM1.Stmt.write a q, v => h_2 a q v
    | Turing.TM1.Stmt.load a q, v => h_3 a q v
    | Turing.TM1.Stmt.branch p q₁ q₂, v => h_4 p q₁ q₂ v
    | Turing.TM1.Stmt.goto l, v => h_5 l v
    | Turing.TM1.Stmt.halt, v => h_6 v) =
    h_1 d q v
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.transEquiv_eq_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : β ≃ γ),
  e.transEquiv e' = e.trans e'.toPartialEquiv
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- An affine combination of covariant derivatives as a covariant derivative.  -/
CovariantDerivative.affineCombination : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [inst_14 : FiberBundle F V] →
                                            CovariantDerivative I F V →
                                              CovariantDerivative I F V → (M → 𝕜) → CovariantDerivative I F V
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.CoextendScalars.map'_hom_apply_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {M M' : ModuleCat R} (g : M ⟶ M')
  (h : ↑((ModuleCat.restrictScalars f).obj (ModuleCat.of S S)) →ₗ[R] ↑M)
  (x : ↑((ModuleCat.restrictScalars f).obj (ModuleCat.of S S))),
  ((ModuleCat.Hom.hom (ModuleCat.CoextendScalars.map' f g)) h) x = (ModuleCat.Hom.hom g) (h x)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharNeTwoNF.a₁ : ∀ {R : Type u_1} {inst : CommRing R} {W : WeierstrassCurve R} [self : W.IsCharNeTwoNF], W.a₁ = 0
-- Init.Data.UInt.Lemmas
UInt16.toFin_inj : ∀ {a b : UInt16}, a.toFin = b.toFin ↔ a = b