mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_X₂ : ∀ {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₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE._auto_3),
  (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₂ = X.cycles f₁ f₂₃ n₁
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.inc_right : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β}, G.IsLink e x y → G.Inc e y
-- Mathlib.Topology.Connected.Clopen
Sigma.isConnected_iff : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {s : Set ((i : ι) × X i)},
  IsConnected s ↔ ∃ i t, IsConnected t ∧ s = Sigma.mk i '' t
-- Init.Data.AC
Lean.Data.AC.Expr.op.injEq : ∀ (lhs rhs lhs_1 rhs_1 : Lean.Data.AC.Expr), (lhs.op rhs = lhs_1.op rhs_1) = (lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.multiplicity_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {p a : α},
  Prime p → FiniteMultiplicity p a → ∀ {k : ℕ}, multiplicity p (a ^ k) = k * multiplicity p a
-- Mathlib.Data.ZMod.Basic
ZMod.neg_val : ∀ {n : ℕ} [NeZero n] (a : ZMod n), (-a).val = if a = 0 then 0 else n - a.val
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coe_inj : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {φ ψ : MvPolynomial σ R}, ↑φ = ↑ψ ↔ φ = ψ
-- Mathlib.Order.Interval.Finset.Defs
Finset.coe_Ico : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α), ↑(Finset.Ico a b) = Set.Ico a b
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instSMul' : {β : Type u_2} → {α : Type u_1} → [SMul β α] → SMul (Lex β) α
-- Batteries.Tactic.Trans
Batteries.Tactic.TransRelation.implies.inj : ∀ {name : Lean.Name} {bi : Lean.BinderInfo} {name_1 : Lean.Name} {bi_1 : Lean.BinderInfo},
  Batteries.Tactic.TransRelation.implies name bi = Batteries.Tactic.TransRelation.implies name_1 bi_1 →
    name = name_1 ∧ bi = bi_1
-- Mathlib.Algebra.Order.Archimedean.Submonoid
AddSubmonoidClass.instAddArchimedean : ∀ {M : Type u_1} {S : Type u_2} [inst : SetLike S M] [inst_1 : AddCommMonoid M] [inst_2 : PartialOrder M]
  [inst_3 : AddSubmonoidClass S M] [Archimedean M] (H : S), Archimedean ↥H
-- Lean.Data.KVMap
/-- Value stored in a key-value map.  -/
Lean.DataValue : Type
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.mk.injEq : ∀ {V : Type u_1} (Adj Adj_1 : V → V → Prop), ({ Adj := Adj } = { Adj := Adj_1 }) = (Adj = Adj_1)
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.supported_eq_vars_subset : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R] {s : Set σ}, ↑(MvPolynomial.supported R s) = {p | ↑p.vars ⊆ s}
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_insertEntry : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {fallback v : β},
  Std.Internal.List.getValueD a (Std.Internal.List.insertEntry k v l) fallback =
    if (k == a) = true then v else Std.Internal.List.getValueD a l fallback
-- Mathlib.Probability.Process.Adapted
MeasureTheory.Filtration.stronglyAdapted_natural : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {β : ι → Type u_3}
  [inst_1 : (i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i}
  [inst_2 : ∀ (i : ι), TopologicalSpace.MetrizableSpace (β i)] [mβ : (i : ι) → MeasurableSpace (β i)]
  [inst_3 : ∀ (i : ι), BorelSpace (β i)] (hum : ∀ (i : ι), MeasureTheory.StronglyMeasurable (u i)),
  MeasureTheory.StronglyAdapted (MeasureTheory.Filtration.natural u hum) u
-- Aesop.Rule
Aesop.instBEqRegularRule : BEq Aesop.RegularRule
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
NNReal.HolderTriple.one_div_nonneg' : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 ≤ 1 / r
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] [inst : Inhabited γ] {f : α → β → Option γ} {k k' : α},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.filterMap f t) k =
        ((Std.DTreeMap.Raw.Const.get? t k).bind fun x => f k' x).get!
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstr.mk.injEq : ∀ (p : Int.Internal.Linear.Poly) (h : Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof) (p_1 : Int.Internal.Linear.Poly)
  (h_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof), ({ p := p, h := h } = { p := p_1, h := h_1 }) = (p = p_1 ∧ h = h_1)
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_shiftLeft : ∀ (a b : ISize) (h : System.Platform.numBits = 32), (a <<< b).toBitVec32 h = a.toBitVec32 h <<< (b.toBitVec32 h).smod 32
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.Rels.alt : {R : Type u} →
  {ι : Type u_4} → {M : Type u_5} → (m : ι → M) → (i j : ι) → m i = m j → i ≠ j → exteriorPower.presentation.Rels R ι M
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'.eq_1 : ∀ {α : Type u_1} {ε : Type u_2} [inst : ENorm ε] {x : MeasurableSpace α} (f : α → ε) (q : ℝ)
  (μ : MeasureTheory.Measure α), MeasureTheory.eLpNorm' f q μ = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
/-- The bivariate polynomials `Ψₙ` congruent to the `n`-division polynomials `ψₙ`.  -/
WeierstrassCurve.Ψ : {R : Type r} → [inst : CommRing R] → WeierstrassCurve R → ℤ → Polynomial (Polynomial R)
-- Mathlib.NumberTheory.Divisors
Nat.image_div_divisors_eq_divisors : ∀ (n : ℕ), Finset.image (fun x => n / x) n.divisors = n.divisors
-- Mathlib.Analysis.Normed.Group.Constructions
MulOpposite.norm_unop : ∀ {E : Type u_2} [inst : SeminormedAddGroup E] (a : Eᵐᵒᵖ), ‖MulOpposite.unop a‖ = ‖a‖
-- Lean.Environment
Lean.EffectiveImport.mk.inj : ∀ {toImport : Lean.Import} {irPhases : Lean.IRPhases} {hasData : Bool} {toImport_1 : Lean.Import}
  {irPhases_1 : Lean.IRPhases} {hasData_1 : Bool},
  { toImport := toImport, irPhases := irPhases, hasData := hasData } =
      { toImport := toImport_1, irPhases := irPhases_1, hasData := hasData_1 } →
    toImport = toImport_1 ∧ irPhases = irPhases_1 ∧ hasData = hasData_1
-- Init.Data.String.Basic
String.Slice.Pos.le_of_not_lt : ∀ {s : String.Slice} {p q : s.Pos}, ¬q < p → p ≤ q
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_unitIso_hom_app_left : ∀ {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] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₁ R),
  ((CategoryTheory.Comma.mapLeftIso R i).unitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.int_mul_sub_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : NonAssocRing α],
  Function.Periodic f c → ∀ (n : ℤ), f (↑n * c - x) = f (-x)
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ringHomComp_ne_one_iff : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {R'' : Type u_3} [inst_2 : CommRing R'']
  {f : R' →+* R''}, Function.Injective ⇑f → ∀ {χ : MulChar R R'}, χ.ringHomComp f ≠ 1 ↔ χ ≠ 1
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.«rule_expr_[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_subset_vadd_left : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t₁ t₂ : Set β}, t₁ ⊆ t₂ → s +ᵥ t₁ ⊆ s +ᵥ t₂
-- Mathlib.Algebra.Order.Module.Defs
OrderDual.instSMulPosStrictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Monoid α] [inst_2 : AddCommGroup β]
  [inst_3 : PartialOrder β] [IsOrderedAddMonoid β] [inst_5 : DistribMulAction α β] [SMulPosStrictMono α β],
  SMulPosStrictMono α βᵒᵈ
-- Init.Data.SInt.Lemmas
Int64.ofNat_div : ∀ {a b : ℕ}, a < 2 ^ 63 → b < 2 ^ 63 → Int64.ofNat (a / b) = Int64.ofNat a / Int64.ofNat b
-- Mathlib.Data.Num.ZNum
Num.div.eq_3 : ∀ (a b : PosNum), (Num.pos a).div (Num.pos b) = a.div' b
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Polynomial.monicEquivDegreeLT.eq_1 : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Nontrivial R] (n : ℕ),
  Polynomial.monicEquivDegreeLT n =
    { toFun := fun p => ⟨(↑p).eraseLead, ⋯⟩, invFun := fun p => ⟨Polynomial.X ^ n + ↑p, ⋯⟩, left_inv := ⋯,
      right_inv := ⋯ }
-- Init.Data.SInt.Lemmas
Int64.lt_or_le : ∀ (a b : Int64), a < b ∨ b ≤ a
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.integral_exp_tilted : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f g : α → ℝ),
  ∫ (x : α), Real.exp (g x) ∂μ.tilted f = (∫ (x : α), Real.exp ((f + g) x) ∂μ) / ∫ (x : α), Real.exp (f x) ∂μ
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Decomposition of an affine map in the special case when the point space and vector space
are the same.  -/
AffineMap.decomp : ∀ {k : Type u_1} {V1 : Type u_2} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddCommGroup V2] [inst_4 : Module k V2] (f : V1 →ᵃ[k] V2), ⇑f = ⇑f.linear + fun x => f 0
-- Mathlib.Analysis.Fourier.LpSpace
SchwartzMap.toLp_fourierInv_eq : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℂ F] [inst_5 : CompleteSpace F]
  [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E] (f : SchwartzMap E F),
  FourierTransformInv.fourierInv (f.toLp 2 MeasureTheory.volume) =
    (FourierTransformInv.fourierInv f).toLp 2 MeasureTheory.volume
-- Mathlib.Algebra.Star.Unitary
Unitary.star_mul_self_of_mem : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {U : R}, U ∈ unitary R → star U * U = 1
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is
less than or equal to the given key.
 -/
Std.ExtDTreeMap.getEntryLE : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] →
        (t : Std.ExtDTreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isLE = true) → (a : α) × β a
-- Init.Data.Range.Polymorphic.SInt
Int16.instRxiIsAlwaysFinite : Std.Rxi.IsAlwaysFinite Int16
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.coe_iSup_of_directed : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {ι : Type u_3} [Nonempty ι]
  {S : ι → StarSubalgebra R A}, Directed (fun x1 x2 => x1 ≤ x2) S → ↑(iSup S) = ⋃ i, ↑(S i)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.isCycle_of_prime_order : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α},
  Nat.Prime (orderOf σ) → σ.support.card < 2 * orderOf σ → σ.IsCycle
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.unitCoeff_coe : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x ≠ 0), ↑↑(PadicInt.unitCoeff hx) = ↑x * ↑p ^ (-↑x.valuation)
-- Init.Data.Vector.Attach
Vector.attachWith.eq_1 : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (P : α → Prop) (H : ∀ x ∈ xs, P x),
  xs.attachWith P H = Vector.mk (xs.toArray.attachWith P ⋯) ⋯
-- Mathlib.Algebra.Algebra.Unitization
NonUnitalAlgHomClass.toNonUnitalAlgHom.congr_simp : ∀ {F : Type u_3} {R : Type u_4} [inst : Monoid R] {A : Type u_5} {B : Type u_6} [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : DistribMulAction R B]
  [inst_5 : FunLike F A B] [inst_6 : NonUnitalAlgHomClass F R A B] (f f_1 : F),
  f = f_1 → NonUnitalAlgHomClass.toNonUnitalAlgHom f = NonUnitalAlgHomClass.toNonUnitalAlgHom f_1
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- `L₃.X₂` is the cokernel of `v₁₂.τ₂ : L₁.X₂ ⟶ L₂.X₂`.  -/
CategoryTheory.ShortComplex.SnakeInput.h₃τ₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex.SnakeInput C) →
        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.v₂₃.τ₂ ⋯)
-- Mathlib.CategoryTheory.Yoneda
/-- If `F` is representable, it is, modulo universe lifting, isomorphic to
`Hom(-, X)` for the representing object `X`.  -/
CategoryTheory.Functor.uliftYonedaReprXIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type (max v v₁))) →
      [inst_1 : F.IsRepresentable] → CategoryTheory.uliftYoneda.{v, v₁, u₁}.obj F.reprX ≅ F
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocContext.level : Lean.VersoModuleDocs.DocContext✝ → ℕ
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) (s : Set 𝕜) (c : F), HasDerivWithinAt (fun x => c) 0 s x
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- Neutral element for addition. It is `0 : ℝ` for the empty basis and `[]` otherwise.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.zero : {basis : Tactic.ComputeAsymptotics.Basis} → Tactic.ComputeAsymptotics.MultiseriesExpansion basis
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOn.sub : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  AnalyticOn 𝕜 f s → AnalyticOn 𝕜 g s → AnalyticOn 𝕜 (f - g) s
-- Mathlib.Algebra.Jordan.Basic
_private.Mathlib.Algebra.Jordan.Basic.0.aux3 : ∀ {A : Type u_1} [inst : NonUnitalNonAssocCommRing A] [IsCommJordan A] {a b c : A},
  ⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (b * b)⁆ + ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (a * a)⁆ +
            2 •
              (⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (a * b)⁆ +
                ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (a * b)⁆) +
          (⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (c * c)⁆ +
              ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (a * a)⁆ +
            2 •
              (⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (c * a)⁆ +
                ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (c * a)⁆)) +
        (⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (c * c)⁆ +
            ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (b * b)⁆ +
          2 •
            (⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (b * c)⁆ +
              ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (b * c)⁆)) +
      (2 • ⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (b * c)⁆ +
          2 • ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (c * a)⁆ +
        2 • ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (a * b)⁆) =
    2 • ⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (b * c)⁆ +
        2 • ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (c * a)⁆ +
      2 • ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (a * b)⁆
-- Init.Data.Vector.Find
Vector.find?_flatten : ∀ {α : Type} {m n : ℕ} {xs : Vector (Vector α m) n} {p : α → Bool},
  Vector.find? p xs.flatten = Vector.findSome? (Vector.find? p) xs
-- Mathlib.Algebra.Algebra.Subalgebra.Operations
instSMulCommClassSubtypeMemSubsemiringSubsemiring : ∀ (B' : Type u_3) [inst : Semiring B'] (G : Type u_4) [inst_1 : Monoid G] [inst_2 : MulSemiringAction G B'],
  SMulCommClass G (↥(FixedPoints.subsemiring B' G)) B'
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
matPolyEquiv_map_C : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  matPolyEquiv (M.map ⇑Polynomial.C) = Polynomial.C M
-- Mathlib.Analysis.InnerProductSpace.NormDet
/-- Using Euclidean Hausdorff measure with the domain dimension, the volume of the image is scaled by
`LinearMap.normDet`.
 -/
LinearMap.euclideanHausdorffMeasure_image : ∀ {U : Type u_5} {V : Type u_6} [inst : NormedAddCommGroup U] [inst_1 : InnerProductSpace ℝ U]
  [inst_2 : FiniteDimensional ℝ U] [inst_3 : NormedAddCommGroup V] [inst_4 : InnerProductSpace ℝ V]
  [inst_5 : MeasurableSpace U] [inst_6 : BorelSpace U] [inst_7 : MeasurableSpace V] [inst_8 : BorelSpace V]
  (f : U →ₗ[ℝ] V) (s : Set U),
  (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) (⇑f '' s) =
    ENNReal.ofReal f.normDet * (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) s
-- Init.Data.Order.Ord
Std.LawfulBEqCmp.mk : ∀ {α : Type u} [inst : BEq α] {cmp : α → α → Ordering},
  (∀ {a b : α}, cmp a b = Ordering.eq ↔ (a == b) = true) → Std.LawfulBEqCmp cmp
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Maps.0.SimpleGraph.Walk.transfer.match_1.eq_2 : ∀ {V : Type u_1} {G : SimpleGraph V} (H : SimpleGraph V)
  (motive : (u v : V) → (p : G.Walk u v) → (∀ e ∈ p.edges, e ∈ H.edgeSet) → Sort u_2) (u w v : V) (h : G.Adj u v)
  (p : G.Walk v w) (h_1 : ∀ e ∈ (SimpleGraph.Walk.cons' u v w h p).edges, e ∈ H.edgeSet)
  (h_1_1 : (u : V) → (h : ∀ e ∈ SimpleGraph.Walk.nil.edges, e ∈ H.edgeSet) → motive u u SimpleGraph.Walk.nil h)
  (h_2 :
    (u w v : V) →
      (h : G.Adj u v) →
        (p : G.Walk v w) →
          (h_2 : ∀ e ∈ (SimpleGraph.Walk.cons' u v w h p).edges, e ∈ H.edgeSet) →
            motive u w (SimpleGraph.Walk.cons h p) h_2),
  (match u, w, SimpleGraph.Walk.cons h p, h_1 with
    | u, .(u), SimpleGraph.Walk.nil, h => h_1_1 u h
    | u, w, SimpleGraph.Walk.cons h p, h_3 => h_2 u w v h p h_3) =
    h_2 u w v h p h_1
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instGroupOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : Group Mᵐᵒᵖ], DomMulAct.instGroupOfMulOpposite = inst
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.equalizerSubobject_arrow_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobject f g).arrow
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobject f g).arrow
      (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.compMonoidHom'_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {γ : Type u_3}
  [inst_2 : TopologicalSpace γ] [inst_3 : MulOneClass γ] [inst_4 : ContinuousMul γ] (g : C(α, β)) (f : C(β, γ)),
  g.compMonoidHom' f = f.comp g
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The (finite) collection of internal stacks  -/
Turing.TM2.Cfg.stk : {K : Type u_1} → {Γ : K → Type u_2} → {Λ : Type u_3} → {σ : Type u_4} → Turing.TM2.Cfg Γ Λ σ → (k : K) → List (Γ k)
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.nth_zero : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (T : Turing.Tape Γ), T.nth 0 = T.head
-- Std.Sync.Broadcast
/-- Creates a new broadcast channel.
 -/
Std.Broadcast.Sync.new : {α : Type} →
  (capacity : optParam ℕ 16) → autoParam (capacity > 0) Std.Broadcast.Sync.new._auto_3 → BaseIO (Std.Broadcast.Sync α)
-- Mathlib.Algebra.Torsor.Defs
Equiv.coe_constVSub : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [inst_1 : AddTorsor G P] (p : P),
  ⇑(Equiv.constVSub p) = fun x => p -ᵥ x
-- Lean.Parser.Types
Lean.Parser.instInhabitedFirstTokens.default : Lean.Parser.FirstTokens
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
/-- A split short complex is short exact.  -/
CategoryTheory.ShortComplex.Splitting.shortExact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting), S.ShortExact
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.contains (t.minKey he) = true
-- Mathlib.Algebra.Group.Units.Defs
/-- Multiplication by a `u : Mˣ` on the left doesn't affect `IsUnit`.  -/
Units.isUnit_units_mul : ∀ {M : Type u_3} [inst : Monoid M] (u : Mˣ) (a : M), IsUnit (↑u * a) ↔ IsUnit a
-- Mathlib.Algebra.Lie.Free
/-- The quotient of `lib R X` by the equivalence relation generated by this relation will give us
the free Lie algebra.  -/
FreeLieAlgebra.Rel : (R : Type u) →
  (X : Type v) → [inst : CommRing R] → FreeNonUnitalNonAssocAlgebra R X → FreeNonUnitalNonAssocAlgebra R X → Prop
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- When a functor `F` preserves the right homology of a short complex `S`, this is the
canonical isomorphism `(S.map F).opcycles ≅ F.obj S.opcycles`.  -/
CategoryTheory.ShortComplex.mapOpcyclesIso : {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 : CategoryTheory.ShortComplex C) →
              (F : CategoryTheory.Functor C D) →
                [inst_4 : F.PreservesZeroMorphisms] →
                  [inst_5 : S.HasRightHomology] →
                    [inst_6 : F.PreservesRightHomologyOf S] → (S.map F).opcycles ≅ F.obj S.opcycles
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
CurveIntegrable.refl : ∀ {𝕜 : 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] (ω : E → E →L[𝕜] F) (a : E),
  CurveIntegrable ω (Path.refl a)
-- Mathlib.Order.Hom.Bounded
BotHom.instPreorder.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : Preorder β] [inst_2 : Bot β],
  BotHom.instPreorder = Preorder.lift DFunLike.coe
-- Mathlib.CategoryTheory.Action.Concrete
Action.ofMulAction_apply : ∀ {G : Type u_1} {H : Type u_2} [inst : Monoid G] [inst_1 : MulAction G H] (g : G) (x : H),
  (CategoryTheory.ConcreteCategory.hom ((Action.ofMulAction G H).ρ g)) x = g • x
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.den_ne_zero : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] (A : Matrix m n ℚ), A.den ≠ 0
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.add_lt_right : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommMonoid M] [Lean.Grind.OrderedAdd M]
  [inst_4 : LT M] [Std.LawfulOrderLT M] {a b : M} (c : M), a < b → c + a < c + b
-- Mathlib.Combinatorics.SimpleGraph.LineGraph
SimpleGraph.map_lineGraph_le_of_le : ∀ {V : Type u_1} {G G' : SimpleGraph V},
  G ≤ G' →
    SimpleGraph.map (⇑(Function.Embedding.subtype fun x => x ∈ G.edgeSet)) G.lineGraph ≤
      SimpleGraph.map (⇑(Function.Embedding.subtype fun x => x ∈ G'.edgeSet)) G'.lineGraph
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.Total.exists_hom_of_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w}
  [inst_1 : CategoryTheory.SmallCategory J] [inst_2 : (j : J) → CategoryTheory.SmallCategory (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} {j j' : J}
  (i : I j) (u : j ⟶ j') [CategoryTheory.IsFiltered (I j')] [CategoryTheory.IsFinitelyPresentable ((P j).diag.obj i)],
  ∃ i' f, f.base = u
-- Mathlib.Data.Nat.Bitwise
Nat.xor_bit : ∀ (a : Bool) (m : ℕ) (b : Bool) (n : ℕ), Nat.bit a m ^^^ Nat.bit b n = Nat.bit (a != b) (m ^^^ n)
-- Mathlib.Analysis.Convex.Extreme
extremePoints_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E], Set.extremePoints 𝕜 ∅ = ∅