mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Split
/-- Number of digits (≥ 4) sufficient for distinguishing anchors. We usually display only the first `numDigits`.  -/
Lean.Meta.Grind.SplitCandidateAnchors.numDigits : Lean.Meta.Grind.SplitCandidateAnchors → ℕ
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.Mono S.v₀₁.τ₁
-- Mathlib.Analysis.ODE.Transform
IsIntegralCurve.comp_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E},
  IsIntegralCurve γ v → ∀ (dt : ℝ), IsIntegralCurve (γ ∘ fun x => x - dt) (v ∘ fun x => x - dt)
-- Mathlib.GroupTheory.Perm.Sign
/-- When the multiset `s : Multiset α` contains all nonfixed points of the permutation `f : Perm α`,
`signAux2 f _` recursively calculates the sign of `f`.  -/
Equiv.Perm.signAux3 : {α : Type u} → [DecidableEq α] → [Finite α] → Equiv.Perm α → {s : Multiset α} → (∀ (x : α), x ∈ s) → ℤˣ
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Converse to the mean value inequality: if `f` is `C`-lipschitz
on a neighborhood of `x₀` then its derivative at `x₀` has norm bounded by `C`. This version
only assumes that `‖f x - f x₀‖ ≤ C * ‖x - x₀‖` in a neighborhood of `x`.  -/
norm_deriv_le_of_lip' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x₀ : 𝕜} {C : ℝ},
  0 ≤ C → (∀ᶠ (x : 𝕜) in nhds x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖) → ‖deriv f x₀‖ ≤ C
-- Mathlib.Computability.Partrec
Computable.of_eq : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f g : α → σ},
  Computable f → (∀ (n : α), f n = g n) → Computable g
-- Mathlib.Analysis.Normed.Module.Bases
SchauderBasis.proj.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (n : ℕ), b.proj n = GeneralSchauderBasis.proj b (Finset.range n)
-- Mathlib.Data.Matrix.Basic
/-- For any algebra `α` over a ring `R`, we have an `R`-algebra isomorphism
`Matₙₓₙ(αᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ` given by transpose.

See also `Matrix.transposeAlgEquiv` for a version that doesn't take the opposite of `α`,
given that its multiplication is commutative.  -/
AlgEquiv.mopMatrix : {m : Type u_2} →
  {R : Type u_7} →
    {α : Type u_11} →
      [inst : Fintype m] →
        [inst_1 : DecidableEq m] →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring α] → [inst_4 : Algebra R α] → Matrix m m αᵐᵒᵖ ≃ₐ[R] (Matrix m m α)ᵐᵒᵖ
-- Mathlib.Topology.UniformSpace.Defs
comp_symm_of_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {s : SetRel α α},
  s ∈ uniformity α → ∃ t ∈ uniformity α, (∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t) ∧ SetRel.comp t t ⊆ s
-- Mathlib.Algebra.Notation.Prod
Prod.instZero.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N], Prod.instZero = { zero := (0, 0) }
-- Init.Data.Vector.MapIdx
Vector.toList_zipIdx : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} (k : optParam ℕ 0), (xs.zipIdx k).toList = xs.toList.zipIdx k
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.sdiv.match_1.eq_2 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match false, true with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_2 ()
-- Mathlib.Data.FinEnum
FinEnum.card_Int8 : FinEnum.card Int8 = 2 ^ 8
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.id_l : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C}
  [inst_1 : Wₗ.ContainsIdentities] [inst_2 : Wᵣ.ContainsIdentities] (c : C),
  (CategoryTheory.Span.id c).l = CategoryTheory.CategoryStruct.id c
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.termNewton_seq : Lean.ParserDescr
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.mk : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      (W : CategoryTheory.MorphismProperty J) →
        (P : CategoryTheory.ObjectProperty J) →
          (∀ {i j : J} {f : i ⟶ j}, W f → P i) →
            (∀ {i j : J} {f : i ⟶ j}, W f → P j) →
              W.HasCardinalLT κ →
                P.HasCardinalLT κ → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.instInhabited : {α : Type u_2} → [inst : TopologicalSpace α] → {x : α} → Inhabited (TopologicalSpace.OpenNhdsOf x)
-- Lean.Environment
/-- The declaration name, known immediately.  -/
Lean.AsyncConstantInfo.name : Lean.AsyncConstantInfo → Lean.Name
-- Mathlib.Topology.Constructions
isOpen_sigma_iff : ∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {s : Set (Sigma σ)},
  IsOpen s ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.deriv_strictMono : ∀ (f : Ordinal.{u_1} → Ordinal.{u_1}), StrictMono (Ordinal.deriv f)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.hom_ext : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} (f g : X ⟶ Y),
  f.left = g.left → f.right = g.right → f = g
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.over_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C}, X ↘ X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.compHom'.eq_1 : ∀ {M : Type uM} {N : Type uN} {P : Type uP} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : CommMonoid P]
  (f : M →* N), f.compHom' = (MonoidHom.eval.comp f).flip
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRightIso_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  (f : X ≅ Y) (g : Y ≅ Z) (W : C),
  CategoryTheory.MonoidalCategory.whiskerRightIso (f ≪≫ g) W =
    CategoryTheory.MonoidalCategory.whiskerRightIso f W ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso g W
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iio_nonempty : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α], (Finset.Iio a).Nonempty ↔ ¬IsMin a
-- Init.Data.BitVec.Lemmas
/-- A sign extension of `x : BitVec w` equals high bits of either `0` or `1` depending on `x.msb`,
followed by the low bits of `x`.  -/
BitVec.signExtend_eq_append_extractLsb' : ∀ {w v : ℕ} {x : BitVec w},
  BitVec.signExtend v x =
    BitVec.cast ⋯ ((if x.msb = true then BitVec.allOnes (v - w) else 0#(v - w)) ++ BitVec.extractLsb' 0 (min w v) x)
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.encard_sdiff_singleton_of_mem`. -/
Set.encard_diff_singleton_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → (s \ {a}).encard = s.encard - 1
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_id : ∀ {𝕜₂ : Type u_6} {F : Type u_10} [inst : NormedField 𝕜₂] [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F], (ContinuousLinearMapWOT.id 𝕜₂ F).toCLM = ContinuousLinearMap.id 𝕜₂ F
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.mapRingHom_id : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α]
  [inst_3 : IsUniformAddGroup α],
  UniformSpace.Completion.mapRingHom (RingHom.id α) ⋯ = RingHom.id (UniformSpace.Completion α)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.subset_one_iff : ∀ {α : Type u_2} [inst : One α] {s : Finset α}, s.Nonempty → (s ⊆ 1 ↔ s = 1)
-- Lean.Syntax
Lean.SourceInfo.getRangeWithTrailing? : optParam Bool false → Lean.SourceInfo → Option Lean.Syntax.Range
-- Mathlib.Analysis.Complex.Exponential
Real.exp_nonneg : ∀ (x : ℝ), 0 ≤ Real.exp x
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.l_biInf_u : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisInsertion l u) {ι : Sort x} {p : ι → Prop} (f : (i : ι) → p i → β),
  l (⨅ i, ⨅ (hi : p i), u (f i hi)) = ⨅ i, ⨅ (hi : p i), f i hi
-- Mathlib.Data.Nat.Init
Nat.AtLeastTwo.one_lt : ∀ {n : ℕ} [n.AtLeastTwo], 1 < n
-- Lean.Language.Basic
/-- Debug description shown by `trace.Elab.snapshotTree`, defaults to the caller's decl name.  -/
Lean.Language.Snapshot.desc : Lean.Language.Snapshot → String
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The isomorphism `t.truncLE a ≅ t.truncLT b` when `a + 1 = b`.  -/
CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT : {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) → (a b : ℤ) → a + 1 = b → (t.truncLE a ≅ t.truncLT b)
-- Init.Data.List.BasicAux
List.tail!_cons : ∀ {α : Type u_1} {a : α} {l : List α}, (a :: l).tail! = l
-- Lean.Parser.Attr
Lean.Parser.Attr.simple.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableWithinAt.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_5} [inst_3 : NormedDivisionRing R] [inst_4 : NormedAlgebra 𝕜 R] {h : E → R}
  {z : E} {S : Set E}, DifferentiableWithinAt 𝕜 h S z → h z ≠ 0 → DifferentiableWithinAt 𝕜 h⁻¹ S z
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.shortComplex_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C), Φ.shortComplex.f = Φ.ι
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasStrictFDerivAt.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {G' : Type u_5} [inst_7 : NormedAddCommGroup G']
  [inst_8 : NormedSpace 𝕜 G'] {f : E → F} {f' : E →L[𝕜] F} {f₂ : G → G'} {f₂' : G →L[𝕜] G'} (p : E × G),
  HasStrictFDerivAt f f' p.1 → HasStrictFDerivAt f₂ f₂' p.2 → HasStrictFDerivAt (Prod.map f f₂) (f'.prodMap f₂') p
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.jb_transform : ∀ (l : Type u_4) (R : Type u₂) [inst : DecidableEq l] [inst_1 : CommRing R] [inst_2 : Fintype l],
  (LieAlgebra.Orthogonal.PB l R).transpose * LieAlgebra.Orthogonal.JB l R * LieAlgebra.Orthogonal.PB l R =
    2 • Matrix.fromBlocks 1 0 0 (LieAlgebra.Orthogonal.S l R)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} [inst_2 : Inhabited (β k)], k ∉ t₁ → (t₁ \ t₂).get! k = default
-- Lean.Meta.AppBuilder
/-- Returns `eq_false h`
`h` must have type definitionally equal to `¬ p` in the current
reducibility setting.  -/
Lean.Meta.mkEqFalse : Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get?.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k' v l r).get? k =
    match h : compare k k' with
    | Ordering.lt => l.get? k
    | Ordering.gt => r.get? k
    | Ordering.eq => some (cast ⋯ v)
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.mul_left : ∀ {n a b : ℕ} (c : ℕ), a ≡ b [MOD n] → c * a ≡ c * b [MOD n]
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β},
  MeasureTheory.AEStronglyMeasurable f μ → ∀ {s : Set α}, MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.liftEquiv_mk : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (N : AddSubgroup G) [nN : N.Normal]
  {φ : G →+ H} (hφ : Function.Surjective ⇑φ) (HN : N = φ.ker) (g : G), (QuotientAddGroup.liftEquiv N hφ HN) ↑g = φ g
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_neg_one_cochain : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cochain F G (-1)),
  CochainComplex.HomComplex.δ (-1) 0 z =
    CochainComplex.HomComplex.Cochain.ofHom (Homotopy.nullHomotopicMap' fun i j hij => z.v i j ⋯)
-- Mathlib.Data.Finset.Sort
Finset.orderEmbOfCardLe_mem : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : k ≤ s.card) (a : Fin k),
  (s.orderEmbOfCardLe h) a ∈ s
-- Mathlib.Order.CompletePartialOrder
/-- Scott-continuity takes on a simpler form in complete partial orders.  -/
CompletePartialOrder.scottContinuous : ∀ {α : Type u_2} {β : Type u_3} [inst : CompletePartialOrder α] [inst_1 : Preorder β] {f : α → β},
  ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))
-- Mathlib.Algebra.Group.Defs
/-- **Alias** of the reverse direction of `isAddCommutative_iff`. -/
IsAddCommutative.of_comm : ∀ {M : Type u_2} [inst : Add M], (∀ (a b : M), a + b = b + a) → IsAddCommutative M
-- Std.Async.Basic
Std.Async.BaseAsync.instMonadFinally : MonadFinally Std.Async.BaseAsync
-- Init.Data.String.Basic
String.slice.eq_1 : ∀ (s : String) (startInclusive endExclusive : s.Pos) (h : startInclusive ≤ endExclusive),
  s.slice startInclusive endExclusive h = s.toSlice.slice startInclusive.toSlice endExclusive.toSlice ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop.0.Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastExtractAndExtend.go : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (assign : α → Bool) (aig : Std.Sat.AIG α) (currIdx w : ℕ)
  (xc : aig.RefVec w) (x : BitVec w) (acc : aig.RefVec (w * currIdx)) (hlt : currIdx ≤ w),
  (∀ (idx : ℕ) (hidx : idx < w * currIdx),
      ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (BitVec.extractAndExtend w x).getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := xc.get idx hidx }⟧ = x.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w * w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go currIdx xc acc hlt ⋯).aig,
              ref :=
                (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go currIdx xc acc hlt ⋯).vec.get idx
                  hidx }⟧ =
          (BitVec.extractAndExtend w x).getLsbD idx
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBMap.alter.adapt.match_3.splitter : {α : Type u_2} →
  {β : Type u_1} →
    (motive : Option (α × β) → Sort u_3) →
      (x : Option (α × β)) → (Unit → motive none) → ((k' : α) → (v' : β) → motive (some (k', v'))) → motive x
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.quasiIsoAt_opFunctor_map_iff : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
  QuasiIsoAt ((HomologicalComplex.opFunctor V c).map φ.op) i ↔ QuasiIsoAt φ i
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ → k ∉ t₁ → k ∈ t₂
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K} (hw : w.IsComplex)
  (x : NumberField.mixedEmbedding.mixedSpace K), (NumberField.mixedEmbedding.normAtPlace w) x = ‖x.2 ⟨w, hw⟩‖
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanModuleHierarchyImportsParams : Lean.ToJson Lean.Lsp.LeanModuleHierarchyImportsParams
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- A homomorphism between isocrystals respects the Frobenius map.
Notation `M →ᶠⁱ [p, k]` in the `Isocrystal` namespace.  -/
WittVector.IsocrystalHom : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (k : Type u_1) →
      [inst_1 : CommRing k] →
        [inst_2 : CharP k p] →
          [inst_3 : PerfectRing k p] →
            (V : Type u_2) →
              [inst_4 : AddCommGroup V] →
                [WittVector.Isocrystal p k V] →
                  (V₂ : Type u_3) → [inst_6 : AddCommGroup V₂] → [WittVector.Isocrystal p k V₂] → Type (max u_2 u_3)
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.lapMatrix.congr_simp : ∀ {V : Type u_1} (R : Type u_2) [inst : Fintype V] (G G_1 : SimpleGraph V),
  G = G_1 →
    ∀ {inst_1 : DecidableRel G.Adj} [inst_2 : DecidableRel G_1.Adj] {inst_3 : DecidableEq V} [inst_4 : DecidableEq V]
      [inst_5 : AddGroupWithOne R] (a a_1 : V),
      a = a_1 → ∀ (a_2 a_3 : V), a_2 = a_3 → SimpleGraph.lapMatrix R G a a_2 = SimpleGraph.lapMatrix R G_1 a_1 a_3
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- Turn an element of a type `F` satisfying `NonUnitalAlgSemiHomClass F φ A B` into an actual
`NonUnitalAlgHom`. This is declared as the default coercion from `F` to `A →ₛₙₐ[φ] B`.  -/
NonUnitalAlgHomClass.toNonUnitalAlgSemiHom : {F : Type u_3} →
  {R : Type u_4} →
    {S : Type u_5} →
      [inst : Monoid R] →
        [inst_1 : Monoid S] →
          {φ : R →* S} →
            {A : Type u_6} →
              {B : Type u_7} →
                [inst_2 : NonUnitalNonAssocSemiring A] →
                  [inst_3 : DistribMulAction R A] →
                    [inst_4 : NonUnitalNonAssocSemiring B] →
                      [inst_5 : DistribMulAction S B] →
                        [inst_6 : FunLike F A B] → [NonUnitalAlgSemiHomClass F φ A B] → F → A →ₛₙₐ[φ] B
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The canonical morphism `X ⟶ functorObj f πX`.  -/
CategoryTheory.SmallObject.ιFunctorObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S X : C} →
            (πX : X ⟶ S) →
              [inst_1 :
                  CategoryTheory.Limits.HasColimitsOfShape
                    (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
                [inst_2 :
                    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
                      (CategoryTheory.SmallObject.functorObjLeft f πX)] →
                  X ⟶ CategoryTheory.SmallObject.functorObj f πX
-- Mathlib.Topology.Spectral.Basic
SpectralSpace.toT0Space : ∀ {X : Type u_3} {inst : TopologicalSpace X} [self : SpectralSpace X], T0Space X
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.nonneg_of_isNat : ∀ {A : Type u_1} {e : A} {n : ℕ} [inst : Semiring A] [inst_1 : PartialOrder A] [IsOrderedRing A],
  Mathlib.Meta.NormNum.IsNat e n → 0 ≤ e
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insertIfNew k v).maxKey ⋯ = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- The left homotopy relation is symmetric.
 -/
SSet.Truncated.HomotopicL.symm : ∀ {X : SSet.Truncated 2} [X.Quasicategory₂]
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f g : SSet.Truncated.Edge x y}, SSet.Truncated.HomotopicL f g → SSet.Truncated.HomotopicL g f
-- Mathlib.Order.ScottContinuity
/-- A function between preorders is said to be Scott continuous if it preserves `IsLUB` on directed
sets. It can be shown that a function is Scott continuous if and only if it is continuous w.r.t. the
Scott topology.
 -/
ScottContinuous : {α : Type u_1} → {β : Type u_2} → [Preorder α] → [Preorder β] → (α → β) → Prop
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.stepAsHetT_filterMapWithPostcondition.match_1.eq_1 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (out' : γ) (h_1 : (out' : γ) → motive (some out'))
  (h_2 : Unit → motive none),
  (match some out' with
    | some out' => h_1 out'
    | none => h_2 ()) =
    h_1 out'
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.snd_comp_inr : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  (OrderMonoidHom.snd α β).comp (OrderMonoidHom.inr α β) = OrderMonoidHom.id β
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceOperator_of_not_memLp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E} [inst_4 : CompleteSpace E],
  ¬MeasureTheory.MemLp id 2 μ → ProbabilityTheory.covarianceOperator μ = 0
-- Mathlib.Order.WellFounded
WellFounded.not_lt_min : ∀ {α : Type u_1} {r : α → α → Prop} (H : WellFounded r) (s : Set α) {x : α} (hx : x ∈ s), ¬r x (H.min s ⋯)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The identity under `X` is initial.  -/
CategoryTheory.Under.mkIdInitial : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} → CategoryTheory.Limits.IsInitial (CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id X))
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instIsArtinianSchemeFiberOfLocallyQuasiFiniteOfQuasiCompact : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f]
  [AlgebraicGeometry.QuasiCompact f] (y : ↥Y),
  AlgebraicGeometry.IsArtinianScheme (AlgebraicGeometry.Scheme.Hom.fiber f y)
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.mem_toLieSubalgebra : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (x : L), x ∈ LieIdeal.toLieSubalgebra R L I ↔ x ∈ I
-- Init.Data.BitVec.Lemmas
BitVec.sub_left_inj : ∀ {w : ℕ} {x y : BitVec w} (z : BitVec w), x - z = y - z ↔ x = y
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.pow : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {φ : MvPolynomial σ R} {m : ℕ},
  φ.IsHomogeneous m → ∀ (n : ℕ), (φ ^ n).IsHomogeneous (m * n)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_symmDiff_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet t μ → μ (symmDiff s t) = μ (s \ t) + μ (t \ s)
-- Mathlib.Order.Basic
LE.ext_iff : ∀ {α : Type u} {x y : LE α}, x = y ↔ LE.le = LE.le
-- Mathlib.Algebra.Order.Group.Abs
eq_of_abs_sub_le_all : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [DenselyOrdered G] {x y : G},
  (∀ ε > 0, |x - y| ≤ ε) → x = y
-- Batteries.Data.List.Lemmas
List.countBefore_lt_count_of_lt_length_of_beq : ∀ {α : Type u_1} {i : ℕ} {x : α} [inst : BEq α] {xs : List α} {h : i < xs.length},
  (xs[i] == x) = true → List.countBefore x xs i < List.count x xs
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Γ'.bit0 : Turing.PartrecToTM2.Γ'