mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- the left type  -/
CategoryTheory.Limits.MulticospanShape.L : CategoryTheory.Limits.MulticospanShape → Type w
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh_nonneg_iff : ∀ {x : ℝ}, 0 ≤ Real.arsinh x ↔ 0 ≤ x
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel_hom_fac : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n)
      (CategoryTheory.CategoryStruct.comp (X.opcyclesIsoKernel f g fg h n).hom
        (CategoryTheory.Limits.kernel.ι ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)))) =
    (X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.OfDiscreteClosed_cell : ∀ {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (hD : IsDiscrete D) (Dc : IsClosed D) (n : ℕ),
  Topology.CWComplex.cell D n =
    match n with
    | 0 => ↑D
    | n.succ => PEmpty.{u_1 + 1}
-- Mathlib.MeasureTheory.Measure.Portmanteau
MeasureTheory.tendsto_of_forall_isClosed_limsup_real_le' : ∀ {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [inst : TopologicalSpace Ω] [inst_1 : OpensMeasurableSpace Ω]
  {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} {L : Filter ι}
  [L.IsCountablyGenerated],
  (∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => (↑(μs i)).real F) L ≤ (↑μ).real F) → Filter.Tendsto μs L (nhds μ)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
UniqueMDiffWithinAt.mono_of_mem_nhdsWithin : ∀ {𝕜 : 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] {s t : Set M} {x : M},
  UniqueMDiffAt[s] x → t ∈ nhdsWithin x s → UniqueMDiffAt[t] x
-- Init.Prelude
/-- Add a new macro scope onto the name `n`, in the given `ctx`.  -/
Lean.addMacroScope : Lean.Name → Lean.Name → Lean.MacroScope → Lean.Name
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.isInteriorPoint_iff : ∀ {𝕜 : 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] {x : M},
  I.IsInteriorPoint x ↔ ↑(extChartAt I x) x ∈ interior (extChartAt I x).target
-- Mathlib.Algebra.Quaternion
/-- `QuaternionAlgebra.imJ` as a `LinearMap`  -/
QuaternionAlgebra.imJₗ : {R : Type u_3} → (c₁ c₂ c₃ : R) → [inst : CommRing R] → QuaternionAlgebra R c₁ c₂ c₃ →ₗ[R] R
-- Init.Data.List.MapIdx
List.getLast?_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : ℕ → α → β},
  (List.mapIdx f l).getLast? = Option.map (f (l.length - 1)) l.getLast?
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instWeakEquivalenceITrivialCofibrationsFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y : C} (f : X ⟶ Y)
  (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f),
  HomotopicalAlgebra.WeakEquivalence h.i
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.all : Lean.Parser.Parser
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.isSolvableAdd : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I J : LieIdeal R L}
  [LieAlgebra.IsSolvable ↥I] [LieAlgebra.IsSolvable ↥J], LieAlgebra.IsSolvable ↥(I + J)
-- Init.Control.ExceptCps
ExceptCpsT.throw_bind : ∀ {m : Type u_1 → Type u_2} {ε α β : Type u_1} [Monad m] (e : ε) (f : α → ExceptCpsT ε m β), throw e >>= f = throw e
-- Mathlib.CategoryTheory.Action.Basic
Action.ρAut_apply_inv : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Group G] (A : Action V G)
  (g : G), (A.ρAut g).inv = A.ρ g⁻¹
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralMulAlgNorm.congr_simp : ∀ (K : Type u) [inst : NontriviallyNormedField K] (L : Type v) [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [inst_4 : CompleteSpace K],
  spectralMulAlgNorm K L = spectralMulAlgNorm K L
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
HomotopicalAlgebra.RelativeCellComplex.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type w'} {inst_1 : LinearOrder J} {inst_2 : OrderBot J}
  {inst_3 : SuccOrder J} {inst_4 : WellFoundedLT J} {α : J → Type t} {A B : (j : J) → α j → C}
  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y}
  {toTransfiniteCompositionOfShape : CategoryTheory.TransfiniteCompositionOfShape J f}
  {attachCells :
    (j : J) →
      ¬IsMax j →
        HomotopicalAlgebra.AttachCells (basicCell j) (toTransfiniteCompositionOfShape.F.map (CategoryTheory.homOfLE ⋯))}
  {toTransfiniteCompositionOfShape_1 : CategoryTheory.TransfiniteCompositionOfShape J f}
  {attachCells_1 :
    (j : J) →
      ¬IsMax j →
        HomotopicalAlgebra.AttachCells (basicCell j)
          (toTransfiniteCompositionOfShape_1.F.map (CategoryTheory.homOfLE ⋯))},
  { toTransfiniteCompositionOfShape := toTransfiniteCompositionOfShape, attachCells := attachCells } =
      { toTransfiniteCompositionOfShape := toTransfiniteCompositionOfShape_1, attachCells := attachCells_1 } →
    toTransfiniteCompositionOfShape = toTransfiniteCompositionOfShape_1 ∧ attachCells ≍ attachCells_1
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertModifier : Std.Time.Modifier → Lean.MacroM (Lean.TSyntax `term)
-- Batteries.Recycling.RBTree.Basic
_private.Batteries.Recycling.RBTree.Basic.0.RBTree.RBNode.fold.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (Unit → motive RBTree.RBNode.nil) →
        ((c : RBTree.RBColor) →
            (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)) →
          motive x
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.eLpNorm_const_smul : ∀ {α : Type u_1} {F : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup F] {𝕜 : Type u_3}
  [inst_1 : NormedDivisionRing 𝕜] [inst_2 : Module 𝕜 F] [NormSMulClass 𝕜 F] (c : 𝕜) (f : α → F) (p : ENNReal)
  (μ : MeasureTheory.Measure α), MeasureTheory.eLpNorm (c • f) p μ = ‖c‖ₑ * MeasureTheory.eLpNorm f p μ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
groupCohomology.δ_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) {i j : ℕ} (hij : i + 1 = j) (z : (Fin i → G) → ↑X.X₃)
  (hz : (CategoryTheory.ConcreteCategory.hom ((groupCohomology.inhomogeneousCochains X.X₃).d i j)) z = 0)
  (y : (Fin i → G) → ↑X.X₂),
  (CategoryTheory.ConcreteCategory.hom ((groupCohomology.cochainsMap (MonoidHom.id G) X.g).f i)) y = z →
    ∀ (x : (Fin j → G) → ↑X.X₁)
      (hx :
        ⇑(Rep.Hom.hom X.f) ∘ x =
          (CategoryTheory.ConcreteCategory.hom ((groupCohomology.inhomogeneousCochains X.X₂).d i j)) y),
      (CategoryTheory.ConcreteCategory.hom (groupCohomology.δ hX i j hij))
          ((CategoryTheory.ConcreteCategory.hom (groupCohomology.π X.X₃ i)) (groupCohomology.cocyclesMk z ⋯)) =
        (CategoryTheory.ConcreteCategory.hom (groupCohomology.π X.X₁ j)) (groupCohomology.cocyclesMkOfCompEqD hX hx)
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
panicking if no such key exists.
 -/
Std.DTreeMap.getKeyGT! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap α β cmp → α → α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.continuous_arctan : Continuous Real.arctan
-- Init.Data.SInt.Float
/-- Truncates a floating-point number to the nearest 8-bit signed integer, rounding towards zero.

If the `Float` is larger than the maximum value for `Int8` (including `Inf`), returns the maximum value of
`Int8` (i.e. `Int8.maxValue`). If it is smaller than the minimum value for `Int8` (including `-Inf`),
returns the minimum value of `Int8` (i.e. `Int8.minValue`). If it is `NaN`, returns `0`.

This function does not reduce in the kernel.
 -/
Float.toInt8 : Float → Int8
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instSemigroup.eq_1 : ∀ {α : Type u_1} [inst : Semigroup α], Colex.instSemigroup = { toMul := Colex.instMul, mul_assoc := ⋯ }
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : DecidableEq ι] {d : ι → R},
  Matrix.diagonal (Sum.elim 0 d) ∈ Submodule.span R (Set.range RootPairing.GeckConstruction.h) ↔
    d ∈ Submodule.span R (Set.range fun i j => ↑(P.pairingIn ℤ j ↑i))
-- Mathlib.Data.Subtype
Subtype.heq_iff_coe_eq : ∀ {α : Sort u_1} {p q : α → Prop},
  (∀ (x : α), p x ↔ q x) → ∀ {a1 : { x // p x }} {a2 : { x // q x }}, a1 ≍ a2 ↔ ↑a1 = ↑a2
-- Mathlib.Data.Seq.Defs
/-- `Seq α` is the type of possibly infinite lists (referred here as sequences).
It is encoded as an infinite stream of options such that if `f n = none`, then
`f m = none` for all `m ≥ n`.  -/
Stream'.Seq : Type u → Type u
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
/-- If a 1-form `ω` is continuous on a set `s`,
then it is curve integrable along any $C^1$ path in this set.  -/
ContinuousOn.curveIntegrable_of_contDiffOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b} [inst_5 : NormedSpace ℝ E] {s : Set E},
  ContinuousOn ω s → ContDiffOn ℝ 1 (⇑γ.extend) unitInterval → (∀ (t : ↑unitInterval), γ t ∈ s) → CurveIntegrable ω γ
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.eq_C_content_mul_primPart : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (p : Polynomial R),
  p = Polynomial.C p.content * p.primPart
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.uncurry_apply : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {M : Type u_3} (x : X)
  (p : ↑(GenLoop M (↑(GenLoop N X x)) GenLoop.const)) (y : (M → ↑unitInterval) × (N → ↑unitInterval)),
  (GenLoop.uncurry x p) y = (p y.1) y.2
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.conjAut_zpow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) (n : ℤ),
  α.conjAut (f ^ n) = α.conjAut f ^ n
-- Mathlib.Tactic.FinCases
/-- Recursively runs the `cases` tactic on a hypothesis `h`.
As long as two goals are produced, `cases` is called recursively on the second goal,
and we return a list of the first goals which appeared.

This is useful for hypotheses of the form `h : a ∈ [l₁, l₂, ...]`,
which will be transformed into a sequence of goals with hypotheses `h : a = l₁`, `h : a = l₂`,
and so on.
Cases are named according to the order in which they are generated as tracked by `counter`
and prefixed with `userNamePre`.
 -/
Lean.Elab.Tactic.unfoldCases : Lean.MVarId → Lean.FVarId → optParam Lean.Name Lean.Name.anonymous → optParam ℕ 0 → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Computability.Encoding
Computability.decode_encodeNum : ∀ (n : Num), Computability.decodeNum (Computability.encodeNum n) = n
-- Mathlib.Data.Part
/-- Converts an `Option α` into a `Part α`.  -/
Part.ofOption : {α : Type u_1} → Option α → Part α
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.State.mk.injEq : ∀ (symbols : Array Lean.HeadIndex) (symbolSet : Std.HashSet Lean.HeadIndex) (bvarsFound : Std.HashSet ℕ)
  (symbols_1 : Array Lean.HeadIndex) (symbolSet_1 : Std.HashSet Lean.HeadIndex) (bvarsFound_1 : Std.HashSet ℕ),
  ({ symbols := symbols, symbolSet := symbolSet, bvarsFound := bvarsFound } =
      { symbols := symbols_1, symbolSet := symbolSet_1, bvarsFound := bvarsFound_1 }) =
    (symbols = symbols_1 ∧ symbolSet = symbolSet_1 ∧ bvarsFound = bvarsFound_1)
-- Mathlib.Data.Set.SMulAntidiagonal
Set.SMulAntidiagonal.eq_of_snd_eq_snd : ∀ {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [inst : SMul G P] {x y : ↑(s.smulAntidiagonal t a)}
  [IsCancelSMul G P], (↑x).2 = (↑y).2 → x = y
-- Mathlib.Algebra.Order.Module.Pointwise
smul_upperBounds_subset_upperBounds_smul_of_nonneg : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
  [PosSMulMono α β] {a : α} {s : Set β}, 0 ≤ a → a • upperBounds s ⊆ upperBounds (a • s)
-- Mathlib.Algebra.Order.Monoid.Lex
/-- Given ordered monoids M, N, the natural projection ordered homomorphism from the
lexicographic M ×ₗ N to M.  -/
OrderMonoidHom.fstₗ : (α : Type u_1) →
  (β : Type u_2) →
    [inst : Monoid α] → [inst_1 : PartialOrder α] → [inst_2 : Monoid β] → [inst_3 : Preorder β] → Lex (α × β) →*o α
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instPow.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β], Colex.instPow = inst
-- Init.Data.String.Lemmas.Splits
/-- You might want to invoke `Pos.Splits.exists_eq_append_singleton` to be able to apply this.  -/
String.Pos.Splits.of_next : ∀ {t₁ : String} {c : Char} {t₂ s : String} {p : s.Pos} {hp : p ≠ s.endPos},
  (p.next hp).Splits (t₁ ++ String.singleton c) t₂ → p.Splits t₁ (String.singleton c ++ t₂)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.dArrowIso₀₁_hom_left : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupCohomology.dArrowIso₀₁ A).hom.left = (groupCohomology.cochainsIso₀ A).hom
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instOne : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [One M] → One (l.Germ M)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α}, k ∉ t₂ → (t₁ ∩ t₂).get? k = none
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
_private.Mathlib.GroupTheory.SpecificGroups.Dihedral.0.DihedralGroup.mul.eq_3 : ∀ {n : ℕ} (a a_1 : ZMod n), DihedralGroup.mul✝ (DihedralGroup.sr a) (DihedralGroup.r a_1) = DihedralGroup.sr (a + a_1)
-- Mathlib.Analysis.Normed.Group.Basic
nndist_nnnorm_nnnorm_le' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (a b : E), nndist ‖a‖₊ ‖b‖₊ ≤ ‖a / b‖₊
-- Mathlib.LinearAlgebra.Finsupp.Supported
/-- `Finsupp.supported M R s` is the `R`-submodule of all `p : α →₀ M` such that `p.support ⊆ s`.  -/
Finsupp.supported : {α : Type u_1} →
  (M : Type u_2) →
    (R : Type u_5) →
      [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Set α → Submodule R (α →₀ M)
-- Mathlib.Algebra.CharP.Algebra
Algebra.ringChar_eq : ∀ (K : Type u_3) (L : Type u_4) [inst : Field K] [inst_1 : CommSemiring L] [Nontrivial L] [Algebra K L],
  ringChar K = ringChar L
-- Init.Data.Vector.Lemmas
Vector.eraseIdx!_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} {h : xs.size = n} {i : ℕ} (hi : i < n),
  (Vector.mk xs h).eraseIdx! i = Vector.mk (xs.eraseIdx i ⋯) ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a : α} {fallback v : β},
      Std.DTreeMap.Raw.Const.getD (t.insert k v) a fallback =
        if cmp k a = Ordering.eq then v else Std.DTreeMap.Raw.Const.getD t a fallback
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
LiouvilleNumber.remainder_pos : ∀ {m : ℝ}, 1 < m → ∀ (k : ℕ), 0 < LiouvilleNumber.remainder m k
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
/-- A comonoid object in the category of `R`-modules has a natural `R`-coalgebra
structure.  -/
CoalgCat.ofComonObj : {R : Type u} → [inst : CommRing R] → (X : ModuleCat R) → [CategoryTheory.ComonObj X] → CoalgCat R
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonParameterInformation : Lean.FromJson Lean.Lsp.ParameterInformation
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instLinear : {S : Type u_1} → [inst : CommRing S] → [inst_1 : TopologicalSpace S] → CategoryTheory.Linear S (TopModuleCat S)
-- Init.Data.Vector.Range
Vector.getElem?_zipIdx : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ}, (xs.zipIdx i)[j]? = Option.map (fun a => (a, i + j)) xs[j]?
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union_aux₂ : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.realSpace K},
  x ≠ 0 →
    x ∈
        ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis ''
          closure (NumberField.mixedEmbedding.fundamentalCone.paramSet K) →
      x ∈ NumberField.mixedEmbedding.fundamentalCone.compactSet K
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.map_subtype_addCommutator : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), AddSubgroup.map H.subtype (addCommutator ↥H) = ⁅H, H⁆
-- Mathlib.LinearAlgebra.Matrix.Determinant.Misc
/-- Let `M` be a `(n+1) × (n+1)` matrix. Assume that all rows, but the `i₀`-row, sums to zero.
Then its determinant is, up to sign, the sum of the `i₀`-row times the determinant of the
matrix obtained by deleting the `i₀`-row and any column.  -/
Matrix.det_eq_sum_row_mul_submatrix_succAbove_succAbove_det : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R) (i₀ j₀ : Fin (n + 1)),
  (∀ (i : Fin (n + 1)), i ≠ i₀ → ∑ j, M i j = 0) →
    M.det = ((-1) ^ (↑i₀ + ↑j₀) * ∑ j, M i₀ j) * (M.submatrix i₀.succAbove j₀.succAbove).det
-- Mathlib.Data.List.Sort
List.sortedLE_map_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, (List.map (⇑OrderDual.ofDual) l).SortedLE ↔ l.SortedGE
-- Init.Data.BitVec.Lemmas
BitVec.not_def : ∀ {v : ℕ} {x : BitVec v}, ~~~x = BitVec.allOnes v ^^^ x
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftsToLimit.toLiftableCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                {c : CategoryTheory.Limits.Cone (K.comp F)} →
                  {t : CategoryTheory.Limits.IsLimit c} →
                    CategoryTheory.LiftsToLimit K F c t → CategoryTheory.LiftableCone K F c
-- Lean.Parser
Lean.PrettyPrinter.Parenthesizer.scientificLit.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.NumberTheory.EulerProduct.ExpLog
/-- If `f : α → ℂ` is summable, then so is `n ↦ log (1 - f n)`.  -/
Summable.clog_one_sub : ∀ {α : Type u_1} {f : α → ℂ}, Summable f → Summable fun n => Complex.log (1 - f n)
-- Mathlib.MeasureTheory.PiSystem
generateFrom_generatePiSystem_eq : ∀ {α : Type u_1} {g : Set (Set α)}, MeasurableSpace.generateFrom (generatePiSystem g) = MeasurableSpace.generateFrom g
-- Lean.Declaration
Lean.ConstructorVal.isUnsafe : Lean.ConstructorVal → Bool
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.congr : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c₁ c₂ : ℝ} {l : Filter α}
  {f₁ f₂ : α → E} {g₁ g₂ : α → F},
  Asymptotics.IsBigOWith c₁ l f₁ g₁ →
    c₁ = c₂ → (∀ (x : α), f₁ x = f₂ x) → (∀ (x : α), g₁ x = g₂ x) → Asymptotics.IsBigOWith c₂ l f₂ g₂
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyMapData.map_φQ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂}
  {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h₁.IsPreservedBy F]
  [inst_6 : h₂.IsPreservedBy F], (ψ.map F).φQ = F.map ψ.φQ
-- Init.Data.Vector.Lemmas
Vector.foldr_eq_foldrM : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β → β} {b : β} {xs : Vector α n},
  Vector.foldr f b xs = (Vector.foldrM (fun x1 x2 => pure (f x1 x2)) b xs).run
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.Equiv.filterWithPostcondition : ∀ {α₁ α₂ β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : Monad n] [inst_3 : LawfulMonad n] [inst_4 : Std.Iterator α₁ m β] [inst_5 : Std.Iterator α₂ m β]
  [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)}
  {ita : Std.IterM m β} {itb : Std.IterM m β},
  ita.Equiv itb → (Std.IterM.filterWithPostcondition f ita).Equiv (Std.IterM.filterWithPostcondition f itb)
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- A subspace of a projective space is a structure consisting of a set of points such that:
If two nonzero vectors determine points which are in the set, and the sum of the two vectors is
nonzero, then the point determined by the sum is also in the set.  -/
Projectivization.Subspace : (K : Type u_1) → (V : Type u_2) → [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [Module K V] → Type u_2
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.instLocallyConnectedSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [LocallyConnectedSpace α],
  LocallyConnectedSpace (TopologicalSpace.Compacts α)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj : ∀ (X : CategoryTheory.Cat) (a : SSet.OneTruncation₂ ((SSet.truncation 2).obj (CategoryTheory.nerve ↑X))),
  (SSet.OneTruncation₂.ofNerve₂.natIso.hom.app X).obj a = SSet.OneTruncation₂.nerveEquiv a
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X)
  (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] {Z : HomotopyCategory D (ComplexShape.down ℕ)}
      (h : F.leftDerivedToHomotopyCategory.obj Y ⟶ Z),
      CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).inv
          (CategoryTheory.CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f) h) =
        CategoryTheory.CategoryStruct.comp
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ))
          (CategoryTheory.CategoryStruct.comp (Q.isoLeftDerivedToHomotopyCategoryObj F).inv h)
-- Mathlib.Analysis.InnerProductSpace.Calculus
differentiable_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E], Differentiable ℝ fun p => inner 𝕜 p.1 p.2
-- Lean.Syntax
Lean.Syntax.mkAntiquotSuffixSpliceNode : Lean.SyntaxNodeKind → Lean.Syntax → String → Lean.Syntax