mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.Const.alter.eq_2 : ∀ {α : Type u} [inst : BEq α] {β : Type v} (a : α) (f : Option β → Option β) (k : α) (v : β)
  (es : Std.DHashMap.Internal.AssocList α fun x => β),
  Std.DHashMap.Internal.AssocList.Const.alter a f (Std.DHashMap.Internal.AssocList.cons k v es) =
    if (k == a) = true then
      match f (some v) with
      | none => es
      | some b => Std.DHashMap.Internal.AssocList.cons a b es
    else
      have tail := Std.DHashMap.Internal.AssocList.Const.alter a f es;
      Std.DHashMap.Internal.AssocList.cons k v tail
-- Batteries.Data.Random.MersenneTwister
/-- Word size (`w`).  -/
Batteries.Random.MersenneTwister.Config.wordSize : Batteries.Random.MersenneTwister.Config → ℕ
-- Batteries.Lean.LawfulMonad
instLawfulMonadEST_batteries : ∀ {ε σ : Type}, LawfulMonad (EST ε σ)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.LHom.realize_onSentence : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type w) [inst : L.Structure M] [inst_1 : L'.Structure M]
  (φ : L →ᴸ L') [φ.IsExpansionOn M] (ψ : L.Sentence), M ⊨ φ.onSentence ψ ↔ M ⊨ ψ
-- Batteries.Control.AlternativeMonad
/-- `failure` is a right identity for `orElse`.  -/
LawfulAlternative.orElse_failure : ∀ {m : Type u_1 → Type u_2} {inst : Alternative m} [self : LawfulAlternative m] {α : Type u_1} (x : m α),
  (x <|> failure) = x
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.consₘ : {α : Type u} →
  {β : α → Type v} →
    [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → β a → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  (CategoryTheory.Abelian.imageStrongEpiMonoFactorisation f).I = CategoryTheory.Abelian.image f
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.coeff_modMonomial_of_le : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s' s : σ →₀ ℕ} (x : MvPolynomial σ R),
  s ≤ s' → MvPolynomial.coeff s' (x.modMonomial s) = 0
-- Mathlib.Algebra.CharZero.Defs
OfNat.one_ne_ofNat : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ) [inst_2 : n.AtLeastTwo], 1 ≠ OfNat.ofNat n
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.coe_liftAlgHom : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_4} [inst_1 : CommRing A] {K : Type u_5} [inst_2 : Field K]
  {L : Type u_7} [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] [inst_6 : Algebra R A]
  [inst_7 : Algebra R K] [inst_8 : IsScalarTower R A K] [inst_9 : Algebra R L] {g : A →ₐ[R] L}
  (hg : Function.Injective ⇑g), ⇑(IsFractionRing.liftAlgHom hg) = ⇑(IsFractionRing.lift hg)
-- Mathlib.Logic.Unique
Unique.mk : {α : Sort u} → (toInhabited : Inhabited α) → (∀ (a : α), a = default) → Unique α
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_sub : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Sub β] (f g : MeasureTheory.SimpleFunc α β),
  ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.preRight.eq_1 : ∀ {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] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (R : CategoryTheory.Functor B T) (F : CategoryTheory.Functor C A)
  (L : CategoryTheory.Functor A T),
  CategoryTheory.Comma.preRight R F L =
    { obj := fun X => { left := X.left, right := F.obj X.right, hom := X.hom },
      map := fun {Y X} f => CategoryTheory.CommaMorphism.mk' (F.map f.right) f.left ⋯, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Topology.MetricSpace.IsometricSMul
dist_smul : ∀ {M : Type u} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : SMul M X] [IsIsometricSMul M X] (c : M) (x y : X),
  dist (c • x) (c • y) = dist x y
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.mem_toSubring : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) (x : K), x ∈ s.toSubring ↔ x ∈ s
-- Mathlib.Algebra.Homology.ExactSequenceFour
/-- If `S` is an exact sequence, this is the isomorphism from the opcycles of `S` in
degree `k + 1` to the cycles of `S` in degree `k + 2`.  -/
CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Balanced C] →
        {n : ℕ} →
          {S : CategoryTheory.ComposableArrows C (n + 3)} →
            (hS : S.Exact) →
              (k : ℕ) →
                (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles._auto_1) →
                  [h₁ : (hS.sc k ⋯).HasRightHomology] →
                    [h₂ : (hS.sc (k + 1) ⋯).HasLeftHomology] → (hS.sc k ⋯).opcycles ≅ (hS.sc (k + 1) ⋯).cycles
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.exp_eq_exp_iff_exp_sub_eq_one : ∀ {x y : ℂ}, Complex.exp x = Complex.exp y ↔ Complex.exp (x - y) = 1
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
/-- The closure of a property of objects of a category under limits of
shape `J a` for a family of categories `J`.  -/
CategoryTheory.ObjectProperty.limitsClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.ObjectProperty C →
      {α : Type t} →
        (J : α → Type u') → [(a : α) → CategoryTheory.Category.{v', u'} (J a)] → CategoryTheory.ObjectProperty C
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.hom_id : ∀ {X : GrpCat}, GrpCat.Hom.hom (CategoryTheory.CategoryStruct.id X) = MonoidHom.id ↑X
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mk.injEq : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (toSubsemiring : Subsemiring A) (algebraMap_mem' : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring.carrier)
  (toSubsemiring_1 : Subsemiring A) (algebraMap_mem'_1 : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring_1.carrier),
  ({ toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' } =
      { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1 }) =
    (toSubsemiring = toSubsemiring_1)
-- Lean.Compiler.LCNF.Types
_private.Lean.Compiler.LCNF.Types.0.Lean.Compiler.LCNF.toLCNFType.visitForall.match_9.eq_1 : ∀ (motive : Lean.Expr → Sort u_1) (n : Lean.Name) (d b : Lean.Expr) (bi : Lean.BinderInfo)
  (h_1 : (n : Lean.Name) → (d b : Lean.Expr) → (bi : Lean.BinderInfo) → motive (Lean.Expr.forallE n d b bi))
  (h_2 : (x : Lean.Expr) → motive x),
  (match Lean.Expr.forallE n d b bi with
    | Lean.Expr.forallE n d b bi => h_1 n d b bi
    | x => h_2 x) =
    h_1 n d b bi
-- Init.Data.Int.Gcd
Int.gcd_sub_mul_left_left : ∀ (m n k : ℤ), (n - m * k).gcd m = n.gcd m
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.zero_rpow_def : ∀ (y : ℝ), 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.canonicalEmbedding.apply_at : ∀ {K : Type u_1} [inst : Field K] (φ : K →+* ℂ) (x : K), (NumberField.canonicalEmbedding K) x φ = φ x
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.instOrderHomClassNat : ∀ {α : Type u_2} [inst : Preorder α], OrderHomClass (OmegaCompletePartialOrder.Chain α) ℕ α
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [inst : Inhabited α] [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ ∪ m₂).get! k = m₁.get! k
-- Mathlib.CategoryTheory.GuitartExact.Basic
/-- When the left and right functors of a 2-square are equivalences, and the natural
transformation of the 2-square is an isomorphism, then the 2-square is Guitart exact.  -/
CategoryTheory.TwoSquare.guitartExact_of_isEquivalence_of_isIso : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  [L.IsEquivalence] [R.IsEquivalence] [CategoryTheory.IsIso w.natTrans], w.GuitartExact
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ},
  R.extEquivCohomologyClass.symm 0 = 0
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_Q : ∀ {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 : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_3),
  (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).right.Q = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
-- Lean.Setup
Lean.ImportArtifacts.oleanPrivate? : Lean.ImportArtifacts → Option System.FilePath
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.instAdditiveObjEvaluation : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} J] (j : J), ((CategoryTheory.evaluation J C).obj j).Additive
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withTop_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β) (a : WithTop α),
  f.withTop a = WithTop.map (⇑f) a
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqns.size : Lean.Meta.Match.MatchEqns → ℕ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceNatCast : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- Extension for the `positivity` tactic: exponentiation by a real number is positive (namely 1)
when the exponent is zero. The other cases are done in `evalRpow`.  -/
Mathlib.Meta.Positivity.evalRpowZero : Mathlib.Meta.Positivity.PositivityExt
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insert!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → ∀ {k : α} {v : β k}, t.isEmpty = true → (Std.DTreeMap.Internal.Impl.insert! k v t).minKey! = k
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.rightIso_inv : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ'),
  (CategoryTheory.Limits.CatCospanTransform.rightIso e).inv = e.inv.right
-- Mathlib.RingTheory.AlgebraicIndependent.Adjoin
/-- The canonical map from the intermediate field generated by an algebraic independent family
into the rational function field.  -/
AlgebraicIndependent.reprField : {ι : Type u_1} →
  {F : Type u_2} →
    {E : Type u_3} →
      {x : ι → E} →
        [inst : Field F] →
          [inst_1 : Field E] →
            [inst_2 : Algebra F E] →
              AlgebraicIndependent F x →
                ↥(IntermediateField.adjoin F (Set.range x)) →ₐ[F] FractionRing (MvPolynomial ι F)
-- Mathlib.Data.Finmap
Finmap.ext_lookup : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s₁ s₂ : Finmap β},
  (∀ (x : α), Finmap.lookup x s₁ = Finmap.lookup x s₂) → s₁ = s₂
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.isIso_opcyclesMap'_of_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.IsIso φ] (h₁ : S₁.RightHomologyData)
  (h₂ : S₂.RightHomologyData), CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂)
-- Mathlib.Algebra.GradedMonoid
/-- Multiplication by `one` on the right is the identity  -/
GradedMonoid.GMonoid.mul_one : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddMonoid ι} [self : GradedMonoid.GMonoid A] (a : GradedMonoid A), a * 1 = a
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.exponent : ∀ {n : ℕ}, Monoid.exponent (QuaternionGroup n) = 2 * lcm n 2
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_image2_eq_csInf_csInf : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [inst_2 : ConditionallyCompleteLattice γ] {s : Set α} {t : Set β}
  {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) →
    (∀ (a : α), GaloisConnection (l₂ a) (u a)) →
      s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sInf (Set.image2 u s t) = u (sInf s) (sInf t)
-- Mathlib.Algebra.DirectSum.Ring
/-- A heavily unfolded version of the definition of multiplication  -/
DirectSum.mul_eq_sum_support_ghas_mul : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] [inst_4 : (i : ι) → (x : A i) → Decidable (x ≠ 0)]
  (a a' : DirectSum ι fun i => A i),
  a * a' =
    ∑ ij ∈ DFinsupp.support a ×ˢ DFinsupp.support a',
      (DirectSum.of A (ij.1 + ij.2)) (GradedMonoid.GMul.mul (a ij.1) (a' ij.2))
-- Std.Data.HashMap.Raw
/-- If there is no mapping for the given key, inserts the given mapping into the map. Otherwise,
returns the map unaltered.
 -/
Std.HashMap.Raw.insertIfNew : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Std.HashMap.Raw α β → α → β → Std.HashMap.Raw α β
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
parallelepiped_basis_eq : ∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  (b : Module.Basis ι ℝ E), parallelepiped ⇑b = {x | ∀ (i : ι), (b.repr x) i ∈ Set.Icc 0 1}
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.inr_injective : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N},
  Function.Injective ⇑SemidirectProduct.inr
-- Lean.Expr
/-- Returns the size of `e` as a tree, i.e. nodes reachable via multiple paths are counted multiple
times.

This is a naive implementation that visits shared subterms multiple times instead of caching their
sizes. It is primarily meant for debugging.
 -/
Lean.Expr.sizeWithoutSharing : Lean.Expr → ℕ
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.mapSubgroup_apply : ∀ {G : Type u_1} [inst : Group G] {H : Type u_6} [inst_1 : Group H] (f : G ≃* H) (H_1 : Subgroup G),
  f.mapSubgroup H_1 = Subgroup.map (↑f) H_1
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- **Alias** of `OpenPartialHomeomorph.coe_mk_symm`. -/
OpenPartialHomeomorph.mk_coe_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (h₁ : ContinuousOn (↑e) e.source) (h₂ : ContinuousOn e.invFun e.target)
  (h₃ : IsOpen { toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ }.source)
  (h₄ : IsOpen { toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ }.target),
  ↑{ toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂, open_source := h₃,
          open_target := h₄ }.symm =
    ↑e.symm
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for subtraction of `BitVec`s.  -/
BitVec.reduceSub : Lean.Meta.Simp.DSimproc
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.one_kronecker : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} [inst : MulZeroOneClass α] [inst_1 : DecidableEq l]
  (B : Matrix m n α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) 1 B =
    (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun x => B)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.isDistinguishedAt_weierstrassDistinguished : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A]
  {g : PowerSeries A} (hg : (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0),
  (g.weierstrassDistinguished hg).IsDistinguishedAt (IsLocalRing.maximalIdeal A)
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- The backward map of an equivalence.

Do NOT use `e.invFun` directly. Use the coercion of `e.symm` instead.  -/
CoalgEquiv.invFun : {R : Type u_5} →
  [inst : CommSemiring R] →
    {A : Type u_6} →
      {B : Type u_7} →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A ≃ₗc[R] B) → B → A
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.trCfg.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (M : Λ → Turing.TM1.Stmt Γ Λ σ) [inst : Inhabited Γ] (l : Option Λ)
  (v : σ) (T : Turing.Tape Γ),
  Turing.TM1to0.trCfg M { l := l, var := v, Tape := T } = { q := (Option.map M l, v), Tape := T }
-- Mathlib.Topology.DiscreteSubset
Set.Infinite.of_accPt : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {S : Set X} {x : X}, AccPt x (Filter.principal S) → S.Infinite
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.bicomp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [inst : TopologicalSpace α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] {f : α → β} {s : Set α} {a : α} [inst_3 : Preorder δ] {op : β → γ → δ},
  Relator.LiftFun (fun x1 x2 => x1 ≤ x2) (Relator.LiftFun (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2) op op →
    IsLocalMaxOn f s a → ∀ {g : α → γ}, IsLocalMaxOn g s a → IsLocalMaxOn (fun x => op (f x) (g x)) s a
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrum.zero_mem : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A] [Nontrivial R]
  (a : A), 0 ∈ quasispectrum R a
-- Lean.Meta.Match.Match
Lean.Meta.Match.processExFalso : Lean.Meta.Match.Problem → Lean.MetaM Lean.Meta.Match.Problem
-- Mathlib.CategoryTheory.FintypeCat
/-- A `Fintype` instance on objects on `FintypeCat`, that should be turned on as needed.
Prefer the `Finite` instance if possible.  -/
FintypeCat.fintype : {X : FintypeCat} → Fintype X.obj
-- Mathlib.Combinatorics.Additive.Corner.Roth
_private.Mathlib.Combinatorics.Additive.Corner.Roth.0.Corners.card_triangleIndices : ∀ {G : Type u_1} [inst : AddCommGroup G] {A : Finset (G × G)}, (Corners.triangleIndices✝ A).card = A.card
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- In an s-finite space, among disjoint measurable sets, only countably many can have positive
measure.  -/
MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion : ∀ {α : Type u_1} {ι : Type u_4} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ]
  {As : ι → Set α},
  (∀ (i : ι), MeasurableSet (As i)) → Pairwise (Function.onFun Disjoint As) → {i | 0 < μ (As i)}.Countable
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ker_ofAlgHom : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {I : Type u_8}
  (f : MvPolynomial I R →ₐ[R] S) (h : Function.Surjective ⇑f),
  (Algebra.Generators.ofAlgHom f h).ker = RingHom.ker f.toRingHom
-- ProofWidgets.Presentation.Expr
ProofWidgets.GetExprPresentationsParams.mk.sizeOf_spec : ∀ (expr : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx), sizeOf { expr := expr } = 1 + sizeOf expr
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpiFamily.uniq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B W : C} {α : Type u_2} (X : α → C)
  (π : (a : α) → X a ⟶ B) [inst_1 : CategoryTheory.EffectiveEpiFamily X π] (e : (a : α) → X a ⟶ W)
  (h :
    ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
      CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
        CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
  (m : B ⟶ W),
  (∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a) → m = CategoryTheory.EffectiveEpiFamily.desc X π e ⋯
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Shifting a configuration commutes with occurrences of a pattern.

Formally: a pattern `p` occurs in the shifted configuration `shift h x` at
position `g` if and only if it occurs in the original configuration `x` at
position `g + h`.  -/
SymbolicDynamics.FullShift.Pattern.occursInAt_shift : ∀ {A : Type u_3} {G : Type u_4} [inst : Inhabited A] [inst_1 : AddMonoid G] (p : SymbolicDynamics.FullShift.Pattern A G)
  (x : G → A) (g h : G), p.occursInAt (SymbolicDynamics.FullShift.shift g x) h ↔ p.occursInAt x (g + h)
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.infinite_compl : ∀ {α : Type u} [Infinite α] {s : Set α}, s.Finite → sᶜ.Infinite
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (Y : T) (X : D)
  (Y_1 : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)),
  ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y_1).right.right =
    Y_1.right.right
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_comap : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R B) (f : F),
  ↑(NonUnitalSubalgebra.comap f S) = ⇑f ⁻¹' ↑S
-- Std.Data.HashSet.Raw
/-- Computes the intersection of the given hash sets. The result will only contain entries from the first map.

This function always merges the smaller set into the larger set, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.HashSet.Raw.inter : {α : Type u} → [BEq α] → [Hashable α] → Std.HashSet.Raw α → Std.HashSet.Raw α → Std.HashSet.Raw α
-- Lean.Meta.Basic
Lean.Meta.DefEqContext.lhs : Lean.Meta.DefEqContext → Lean.Expr
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.lanCompIsoOfPreserves_hom_app : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (L : CategoryTheory.Functor A C)
  [inst_4 : G.PreservesLeftKanExtensions L] [inst_5 : ∀ (F : CategoryTheory.Functor A B), L.HasLeftKanExtension F]
  [inst_6 : ∀ (F : CategoryTheory.Functor A D), L.HasLeftKanExtension F] (X : CategoryTheory.Functor A B),
  (G.lanCompIsoOfPreserves L).hom.app X = (G.leftKanExtensionCompIsoOfPreserves X L).hom
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.coePiBasisFun.toMatrix_eq_transpose : ∀ {ι : Type u_1} {R : Type u_5} [inst : CommSemiring R] [inst_1 : Finite ι],
  (Pi.basisFun R ι).toMatrix = Matrix.transpose