mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
_private.Mathlib.RingTheory.Extension.Cotangent.BaseChange.0.Algebra.tensorH1CotangentOfFlat.eq_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Module.Flat R T],
  Algebra.tensorH1CotangentOfFlat R S T =
    (((Algebra.Generators.self R S).toExtension.tensorH1CotangentOfFlat T).trans
          (LinearEquiv.restrictScalars T
            (Algebra.Extension.H1Cotangent.equiv ((Algebra.Generators.self R S).baseChangeFromBaseChange T)
              ((Algebra.Generators.self R S).baseChangeToBaseChange T)))).trans
      (LinearEquiv.restrictScalars T (Algebra.Generators.baseChange T (Algebra.Generators.self R S)).equivH1Cotangent)
-- Mathlib.Data.Finset.Image
Finset.image_id : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α], Finset.image id s = s
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.isSelfAdjoint : ∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : StarAddMonoid R] {x : ↥(selfAdjoint R)}, IsSelfAdjoint ↑x
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι] {Z : C} (h : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).hom
      (CategoryTheory.CategoryStruct.comp S.homologyι h) =
    CategoryTheory.CategoryStruct.comp ι (CategoryTheory.CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).hom h)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_inter_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k fallback : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.inter m₂ ⋯).getKeyD k fallback = fallback
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toListRev_eq_match_step : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.toListRev =
    match ↑it.step with
    | Std.IterStep.yield it' out => it'.toListRev ++ [out]
    | Std.IterStep.skip it' => it'.toListRev
    | Std.IterStep.done => []
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.HasLeftHomology.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData), S.HasLeftHomology
-- Mathlib.Analysis.LocallyConvex.AbsConvex
closure_subset_closedAbsConvexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] [inst_4 : TopologicalSpace E] {s : Set E}, closure s ⊆ (closedAbsConvexHull 𝕜) s
-- Mathlib.Logic.Function.OfArity
Function.OfArity.const_succ : ∀ (α : Type u) {β : Type u} (b : β) (n : ℕ), Function.OfArity.const α b n.succ = fun x => Function.OfArity.const α b n
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasStrictFDerivAt_sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : F} (c : F), HasStrictFDerivAt (fun x => x - c) (ContinuousLinearMap.id 𝕜 F) x
-- Mathlib.Analysis.SpecialFunctions.NonIntegrable
/-- The function `fun x => (x - c)⁻¹` is integrable on `a..b` if and only if
`a = b` or `c ∉ [a, b]`.  -/
intervalIntegrable_sub_inv_iff : ∀ {a b c : ℝ}, IntervalIntegrable (fun x => (x - c)⁻¹) MeasureTheory.volume a b ↔ a = b ∨ c ∉ Set.uIcc a b
-- Init.Data.Order.Lemmas
Std.min_le : ∀ {α : Type u} [inst : Min α] [inst_1 : LE α] [Std.IsPreorder α] [Std.LawfulOrderMin α] {a b c : α},
  a ⊓ b ≤ c ↔ a ≤ c ∨ b ≤ c
-- Mathlib.RingTheory.Polynomial.Pochhammer
_private.Mathlib.RingTheory.Polynomial.Pochhammer.0.ascPochhammer.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Init.Data.BitVec.Lemmas
BitVec.append_right_inj : ∀ {w w' : ℕ} (s : BitVec w) {t₁ t₂ : BitVec w'}, s ++ t₁ = s ++ t₂ ↔ t₁ = t₂
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.π_naturality_assoc : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) (X Y : A) (f : X ⟶ Y) {Z : A} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ι.map (Λ.F.map f)) (CategoryTheory.CategoryStruct.comp (Λ.π.app Y) h) =
    CategoryTheory.CategoryStruct.comp (Λ.π.app X) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.coeff_add_of_disjoint : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [hp : Fact (Nat.Prime p)] (x y : WittVector p R),
  (∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0) → (x + y).coeff n = x.coeff n + y.coeff n
-- Batteries.Data.List.Lemmas
List.countPBefore_cons_succ : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {i : ℕ} {a : α},
  List.countPBefore p (a :: xs) (i + 1) = if p a = true then List.countPBefore p xs i + 1 else List.countPBefore p xs i
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.closure_univ : ∀ {K : Type u} [inst : DivisionRing K], Subfield.closure Set.univ = ⊤
-- Mathlib.LinearAlgebra.Reflection
/-- A formula for $r_2 (r_1 r_2)^m x$, where $m$ is an integer.  -/
Module.reflection_mul_reflection_mul_reflection_zpow_apply_self : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M}
  {f g : Module.Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℤ) (t : optParam R (f y * g x - 2)),
  autoParam (t = f y * g x - 2) Module.reflection_mul_reflection_mul_reflection_zpow_apply_self._auto_1 →
    (Module.reflection hg * (Module.reflection hf * Module.reflection hg) ^ m) x =
      (Polynomial.eval t (Polynomial.Chebyshev.S R m) + Polynomial.eval t (Polynomial.Chebyshev.S R (m - 1))) • x +
        (Polynomial.eval t (Polynomial.Chebyshev.S R m) * -g x) • y
-- Mathlib.Data.Fintype.Card
Fintype.card_le_of_embedding : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α ↪ β), Fintype.card α ≤ Fintype.card β
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Result.mk.inj : ∀ {failure? : Option Lean.Meta.Grind.Goal} {issues : List Lean.MessageData} {config : Lean.Grind.Config}
  {counters : Lean.Meta.Grind.Counters} {simp : Lean.Meta.Simp.Stats}
  {splitDiags : Lean.PArray Lean.Meta.Grind.SplitDiagInfo} {ematchDiags : Lean.PArray Lean.Meta.Grind.EMatchDiagInfo}
  {failure?_1 : Option Lean.Meta.Grind.Goal} {issues_1 : List Lean.MessageData} {config_1 : Lean.Grind.Config}
  {counters_1 : Lean.Meta.Grind.Counters} {simp_1 : Lean.Meta.Simp.Stats}
  {splitDiags_1 : Lean.PArray Lean.Meta.Grind.SplitDiagInfo}
  {ematchDiags_1 : Lean.PArray Lean.Meta.Grind.EMatchDiagInfo},
  { failure? := failure?, issues := issues, config := config, counters := counters, simp := simp,
        splitDiags := splitDiags, ematchDiags := ematchDiags } =
      { failure? := failure?_1, issues := issues_1, config := config_1, counters := counters_1, simp := simp_1,
        splitDiags := splitDiags_1, ematchDiags := ematchDiags_1 } →
    failure? = failure?_1 ∧
      issues = issues_1 ∧
        config = config_1 ∧
          counters = counters_1 ∧ simp = simp_1 ∧ splitDiags = splitDiags_1 ∧ ematchDiags = ematchDiags_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.not_mem_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α}, k ∉ ∅
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.Decidable.instStrictBackwardPatternForallCharProp : ∀ {p : Char → Prop} [inst : DecidablePred p], String.Slice.Pattern.StrictBackwardPattern p
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `FunLike.coeAddMonoidHom`. -/
QuadraticMap.coeFnAddMonoidHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) →
      [inst : FunLike F α β] →
        [inst_1 : AddZero F] → [inst_2 : AddZeroClass β] → [IsZeroApply F α β] → [IsAddApply F α β] → F →+ α → β
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_add_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T T' T'' : Set α → E →L[ℝ] F),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s) →
    ∀ (f : ↥(α →₁ₛ[μ] E)),
      MeasureTheory.L1.SimpleFunc.setToL1S T'' f =
        MeasureTheory.L1.SimpleFunc.setToL1S T f + MeasureTheory.L1.SimpleFunc.setToL1S T' f
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_sep_self : ∀ {α : Type u_1} (s : Set α) (p : α → Prop), s \ {a | a ∈ s ∧ p a} = {a | a ∈ s ∧ ¬p a}
-- Mathlib.SetTheory.ZFC.Class
Class.coe_sep : ∀ (p : Class.{u}) (x : ZFSet.{u}), ↑(ZFSet.sep p x) = {y | y ∈ x ∧ p y}
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.opEquiv.match_13.eq_1 : ∀ (C : Type u_1) (motive : CategoryTheory.WithTerminal Cᵒᵖ → Sort u_2) (x : Cᵒᵖ)
  (h_1 : (x : Cᵒᵖ) → motive (CategoryTheory.WithTerminal.of x)) (h_2 : Unit → motive CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.of x with
    | CategoryTheory.WithTerminal.of x => h_1 x
    | CategoryTheory.WithTerminal.star => h_2 ()) =
    h_1 x
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
CategoryTheory.Pseudofunctor.IsPrestack.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  {J : CategoryTheory.GrothendieckTopology C},
  (∀ {S : C} (M N : ↑(F.obj { as := Opposite.op S })), CategoryTheory.Presheaf.IsSheaf (J.over S) (F.presheafHom M N)) →
    F.IsPrestack J
-- Mathlib.NumberTheory.Height.NumberField
/-- If `x : K` (for a number field `K`), then we can find a nonzero `n : ℕ` such that
`n ≤ mulHeight₁ x` and `n * x` is integral. I.e., the denominator of `x` can be bounded by
its multplicative height.  -/
NumberField.exists_nat_le_mulHeight₁ : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : K),
  ∃ n, n ≠ 0 ∧ ↑n ≤ Height.mulHeight₁ x ∧ IsIntegral ℤ (↑n * x)
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.lt_two_pow_of_le : ∀ {x m n : ℕ}, x < 2 ^ m → m ≤ n → x < 2 ^ n
-- Mathlib.CategoryTheory.Localization.Predicate
/-- Via the equivalence of categories `equivalenceFromModel L W : W.Localization ≌ D`,
one may identify the functors `L` and `W.Q`.  -/
CategoryTheory.Localization.compEquivalenceFromModelInverseIso : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : L.IsLocalization W] → L.comp (CategoryTheory.Localization.equivalenceFromModel L W).inverse ≅ W.Q
-- Std.Data.DTreeMap.Raw.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.DTreeMap.Raw.Const.toArray : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → Array (α × β)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.const_nsmul : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : AddMonoid β] [ContinuousAdd β],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (n • f) μ
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mrange_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mrange (AddMonoidHom.inl M N) = ⊤.prod ⊥
-- Lean.Meta.AppBuilder
Lean.Meta.mkImpDepCongrCtx : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Basic
inv_surjective : ∀ {G : Type u_3} [inst : InvolutiveInv G], Function.Surjective Inv.inv
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
cyclotomicCharacter.toZModPow_toFun : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] (g : L ≃+* L)
  [inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)] (n : ℕ),
  (PadicInt.toZModPow n) (cyclotomicCharacter.toFun p g) = ↑((modularCyclotomicCharacter L ⋯) g)
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.of_shrink : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Small.{v', v} M] [Module.Flat R (Shrink.{v', v} M)], Module.Flat R M
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.sieveOfSubfunctor_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
  (f : R ⟶ CategoryTheory.yoneda.obj X) (Y : C) (g : Y ⟶ X),
  (CategoryTheory.Sieve.sieveOfSubfunctor f).arrows g =
    ∃ t, (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op Y))) t = g
-- Init.Data.Array.Lemmas
Array.map_const : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {b : β}, Array.map (Function.const α b) xs = Array.replicate xs.size b
-- Mathlib.Analysis.Normed.Ring.Basic
NormedCommRing.mk : {α : Type u_5} → [toNormedRing : NormedRing α] → (∀ (a b : α), a * b = b * a) → NormedCommRing α
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instInhabitedPartialMatch.default : Lean.Meta.LazyDiscrTree.PartialMatch
-- Mathlib.Computability.Ackermann
/-- Yields single recursion step on `pappAck`.  -/
Nat.Partrec.Code.pappAck.step : Nat.Partrec.Code → Nat.Partrec.Code
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor set of `v` is disjoint to `s`.  -/
SimpleGraph.isBipartiteWith_neighborSet_disjoint : ∀ {V : Type u_1} {v : V} {G : SimpleGraph V} {s t : Set V}, G.IsBipartiteWith s t → v ∈ s → Disjoint (G.neighborSet v) s
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- `p.firstReturn` is 0 if `p = 0` and the index of the `D` matching the initial `U` otherwise.  -/
DyckWord.firstReturn : DyckWord → ℕ
-- Lean.Elab.DeclModifiers
Lean.Elab.checkIfShadowingStructureField : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → m Unit
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_inv_app_right_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  (X_1 : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)),
  ((CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso α β X).inv.app X_1).right.left =
    CategoryTheory.CategoryStruct.id X_1.right.left
-- Init.Data.List.Nat.TakeDrop
/-- Taking the first `i` elements in `l₁ ++ l₂` is the same as appending the first `i` elements
of `l₁` to the first `n - l₁.length` elements of `l₂`.  -/
List.take_append : ∀ {α : Type u_1} {l₁ l₂ : List α} {i : ℕ}, List.take i (l₁ ++ l₂) = List.take i l₁ ++ List.take (i - l₁.length) l₂
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_pos : ∀ {E : Type u_5} [inst : NormedAddGroup E] {a : E}, 0 < ‖a‖₊ ↔ a ≠ 0
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_subset_adjoin_iff : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {F' : Type u_3}
  [inst_3 : Field F'] [inst_4 : Algebra F' E] {S S' : Set E},
  ↑(IntermediateField.adjoin F S) ⊆ ↑(IntermediateField.adjoin F' S') ↔
    Set.range ⇑(algebraMap F E) ⊆ ↑(IntermediateField.adjoin F' S') ∧ S ⊆ ↑(IntermediateField.adjoin F' S')
-- Mathlib.Data.PNat.Xgcd
/-- The `Repr` instance converts terms to strings in a way that
reflects the matrix/vector interpretation as above.  -/
PNat.XgcdType.instRepr : Repr PNat.XgcdType
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.isEqv.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → (α → α → Bool) → Sort u_2) (a : α) (as : List α) (b : α) (bs : List α)
  (eqv : α → α → Bool) (h_1 : (x : α → α → Bool) → motive [] [] x)
  (h_2 : (a : α) → (as : List α) → (b : α) → (bs : List α) → (eqv : α → α → Bool) → motive (a :: as) (b :: bs) eqv)
  (h_3 : (x x_1 : List α) → (x_2 : α → α → Bool) → motive x x_1 x_2),
  (match a :: as, b :: bs, eqv with
    | [], [], x => h_1 x
    | a :: as, b :: bs, eqv => h_2 a as b bs eqv
    | x, x_1, x_2 => h_3 x x_1 x_2) =
    h_2 a as b bs eqv
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.congr : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f g : α → β},
  Filter.EventuallyConst f l → f =ᶠ[l] g → Filter.EventuallyConst g l
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_filter!_key : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool}
  {k fallback : α},
  t.WF →
    (Std.DTreeMap.Internal.Impl.filter! (fun k x => f k) t).getKeyD k fallback =
      (Option.filter f (t.getKey? k)).getD fallback
-- Mathlib.Data.Set.Opposite
Set.singleton_op : ∀ {α : Type u_1} (x : α), {x}.op = {Opposite.op x}
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.subringClass : ∀ {R : Type u_6} {A : Type u_7} [inst : CommRing R] [inst_1 : StarRing R] [inst_2 : Ring A] [inst_3 : StarRing A]
  [inst_4 : Algebra R A] [inst_5 : StarModule R A], SubringClass (StarSubalgebra R A) A
-- Mathlib.RingTheory.Multiplicity
emultiplicity_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {p a : α},
  Prime p → ∀ {k : ℕ}, emultiplicity p (a ^ k) = ↑k * emultiplicity p a
-- Mathlib.RingTheory.Binomial
Ring.map_choose : ∀ {R : Type u_2} {S : Type u_3} {F : Type u_4} [inst : Ring R] [inst_1 : Ring S] [inst_2 : BinomialRing R]
  [inst_3 : BinomialRing S] [inst_4 : FunLike F R S] [RingHomClass F R S] (f : F) (a : R) (n : ℕ),
  f (Ring.choose a n) = Ring.choose (f a) n
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  {f g : α ≃+o β}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.Order.Interval.Set.Basic
Set.Ioi_subset_Ici_self : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Ioi a ⊆ Set.Ici a
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.hasPullback_of_left : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f], CategoryTheory.Limits.HasPullback f g
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- A SubMulAction is a set which is closed under scalar multiplication.  -/
SubMulAction : (R : Type u) → (M : Type v) → [SMul R M] → Type v
-- Mathlib.Algebra.Group.Action.Defs
inv_smul_smul : ∀ {G : Type u_3} {α : Type u_5} [inst : Group G] [inst_1 : MulAction G α] (g : G) (a : α), g⁻¹ • g • a = a
-- Mathlib.Order.WithBot
WithBot.LT.bot_lt : ∀ {α : Type u_1} [inst : LT α] (b : α), ⊥.LT ↑b
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.instBot : {R : Type u} → [inst : NonAssocRing R] → Bot (Subring R)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.horizontalComp.sizeOf_spec : ∀ (e : Lean.Expr) (f₁ g₁ f₂ g₂ : Mathlib.Tactic.BicategoryLike.Mor₁) (η θ : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂Iso.horizontalComp e f₁ g₁ f₂ g₂ η θ) =
    1 + sizeOf e + sizeOf f₁ + sizeOf g₁ + sizeOf f₂ + sizeOf g₂ + sizeOf η + sizeOf θ
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.toSimprocEntry : Lean.Meta.Simp.SimprocOLeanEntry → Lean.ImportM Lean.Meta.Simp.SimprocEntry
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.coneMorphism_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (c : CategoryTheory.Limits.Cone F)
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.coneMorphism c).hom
      (CategoryTheory.Limits.limit.π F j) =
    c.π.app j
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.fourierTransformCLM_apply : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℂ E]
  [inst_3 : NormedSpace 𝕜 E] [inst_4 : SMulCommClass ℂ 𝕜 E] {V : Type u_3} [inst_5 : NormedAddCommGroup V]
  [inst_6 : InnerProductSpace ℝ V] [inst_7 : FiniteDimensional ℝ V] [inst_8 : MeasurableSpace V] [inst_9 : BorelSpace V]
  (f : SchwartzMap V E), (SchwartzMap.fourierTransformCLM 𝕜) f = FourierTransform.fourier f
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.hasPrev.eq_1 : ∀ (s : String) (i : String.Pos.Raw), { s := s, i := i }.hasPrev = decide (i.byteIdx > 0)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHint.toCustomInfo : Lean.Elab.InlayHint → Lean.Elab.CustomInfo
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_add_right_zero : ∀ {α : Type u_2} [inst : AddGroup α] {b : α}, (fun x => x + b) ⁻¹' 0 = {-b}
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
/-- Auxiliary definition for `LeftResolution.karoubi`.  -/
CategoryTheory.Abelian.LeftResolution.karoubi.F' : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} →
          CategoryTheory.Abelian.LeftResolution ι →
            [CategoryTheory.Preadditive C] →
              [CategoryTheory.Preadditive A] → CategoryTheory.Functor A (CategoryTheory.Idempotents.Karoubi C)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.basicOpen_pow : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) (n : ℕ),
  0 < n → ProjectiveSpectrum.basicOpen 𝒜 (f ^ n) = ProjectiveSpectrum.basicOpen 𝒜 f
-- Mathlib.MeasureTheory.Measure.Dirac
HasSum.isProbabilityMeasure_sum_dirac_nnreal : ∀ {δ : Type u_3} {ι : Type u_4} {mδ : MeasurableSpace δ} {c : ι → NNReal} {d : ι → δ},
  HasSum c 1 →
    MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.sum fun i => c i • MeasureTheory.Measure.dirac (d i))