mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.closure_union : ∀ {M : Type u_1} [inst : AddZeroClass M] (s t : Set M),
  AddSubmonoid.closure (s ∪ t) = AddSubmonoid.closure s ⊔ AddSubmonoid.closure t
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instAddCommMagmaQuotient : {R : Type u_1} → [inst : AddCommMagma R] → [inst_1 : Mul R] → (c : RingCon R) → AddCommMagma c.Quotient
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
/-- The shifted resolution of a topological representation by `1` degree.  -/
TopRep.resolution' : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] →
      [inst_1 : Group G] →
        [inst_2 : TopologicalSpace k] →
          [inst_3 : TopologicalSpace G] → [IsTopologicalGroup G] → TopRep k G → CochainComplex (TopRep k G) ℕ
-- Mathlib.Logic.Relation
Relation.SymmGen.of_rel_symm : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, r b a → Relation.SymmGen r a b
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.completeSpace : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → UniformSpace (β i)]
  [∀ (i : ι), CompleteSpace (β i)], CompleteSpace (PiLp p β)
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.hasSum_qExpansion : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
      MDiff f →
        UpperHalfPlane.IsBoundedAtImInfty f →
          ∀ (τ : UpperHalfPlane),
            HasSum (fun m => (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h f) • Function.Periodic.qParam h ↑τ ^ m)
              (f τ)
-- Lean.Elab.Tactic.SimpTrace
/-- Implementation of `dsimp?`.  -/
Lean.Elab.Tactic.dsimpLocation' : Lean.Meta.Simp.Context →
  Lean.Meta.Simp.SimprocsArray → Lean.Elab.Tactic.Location → Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Stats
-- Lean.LibrarySuggestions.SineQuaNon
/-- This isn't exactly what's described in the paper.

We select theorems in a priority order, where the priority is `1.5 ^ (trigger depth) * Π (tolerances)`.

The `1.5` factor could be tuned.
 -/
Lean.LibrarySuggestions.SineQuaNon.sineQuaNon : Lean.NameSet → ℕ → optParam Float 1.5 → optParam Float 1e-2 → Lean.MetaM (Array Lean.LibrarySuggestions.Suggestion)
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctor'_hom_app_τ₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ),
  ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₂ =
    (HomologicalComplex.XIsoOfEq X ⋯).hom
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.Ref.not.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} (ref : aig.Ref), ref.not = ref.flip true
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The arrow choice for each pair of vertices  -/
CategoryTheory.Subgroupoid.arrows : {C : Type u} → [inst : CategoryTheory.Groupoid C] → CategoryTheory.Subgroupoid C → (c d : C) → Set (c ⟶ d)
-- Mathlib.Computability.TuringMachine.Computable
/-- **Alias** of `StateTransition.EvalsToInTime`. -/
Turing.EvalsToInTime : {σ : Type u_1} → (σ → Option σ) → σ → Option σ → ℕ → Type
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.ofSubmodule_inj : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] {S T : Submodule R E}, ↑S = ↑T ↔ S = T
-- Batteries.Recycling.MonadSatisfying.Basic
_private.Batteries.Recycling.MonadSatisfying.Basic.0.SatisfiesM_EStateM_eq.match_1_3.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s' : σ) → x = EStateM.Result.ok a s' → motive (EStateM.Result.ok a s')) →
        ((e : ε) → (s' : σ) → x = EStateM.Result.error e s' → motive (EStateM.Result.error e s')) → motive x
-- Mathlib.Algebra.Group.Basic
nsmul_add_nsmul_eq_zero : ∀ {M : Type u_4} [inst : AddMonoid M] {a b : M} (n : ℕ), a + b = 0 → n • a + n • b = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited α] {f : α → β → Option γ} {k : α} (h : t.WF),
  (Std.TreeMap.Raw.filterMap f t).getKey! k = ((t.getKey? k).pfilter fun x h' => (f x t[x]).isSome).get!
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.coe_add : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {x y : ℚ}, ↑(x + y) = ↑x + ↑y
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.fromLocalizedModule.inj : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f], Function.Injective ⇑(IsLocalizedModule.fromLocalizedModule S f)
-- Mathlib.Topology.Basic
isOpen_iUnion : ∀ {X : Type u} {ι : Sort v} [inst : TopologicalSpace X] {f : ι → Set X}, (∀ (i : ι), IsOpen (f i)) → IsOpen (⋃ i, f i)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Collector.State.mk : Array Lean.Expr → Bool → Lean.Meta.Grind.Collector.State✝
-- Std.Data.Internal.Cut
Std.Internal.IsStrictCut : {α : Type u} → (α → α → Ordering) → (α → Ordering) → Prop
-- Mathlib.Data.Set.Lattice
Set.compl_iInter : ∀ {β : Type u_2} {ι : Sort u_5} (s : ι → Set β), (⋂ i, s i)ᶜ = ⋃ i, (s i)ᶜ
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.Ici_add_bij : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a d : M), Set.BijOn (fun x => x + d) (Set.Ici a) (Set.Ici (a + d))
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_toUInt64 : ∀ (n : UInt32), n.toUInt64.toUInt16 = n.toUInt16
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- A `WeakFEPair` structure with `f = evenKernel a` and `g = cosKernel a`.  -/
HurwitzZeta.hurwitzEvenFEPair : UnitAddCircle → WeakFEPair ℂ
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.approxOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α]
  [inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] (f : β → α) (hf : Measurable f) (s : Set α) (y₀ : α)
  (h₀ : y₀ ∈ s) [inst_4 : TopologicalSpace.SeparableSpace ↑s] (n : ℕ),
  MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n =
    (MeasureTheory.SimpleFunc.nearestPt (fun k => Nat.casesOn k y₀ (Subtype.val ∘ TopologicalSpace.denseSeq ↑s)) n).comp
      f hf
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrSet_symm_apply : ∀ {α : Type u_11} {W : α → Sort w} {s t : Set α} (h : s = t) (f : (i : { i // i ∈ t }) → W ↑i) (i : { i // i ∈ s }),
  (Equiv.piCongrSet h).symm f i = f ⟨↑i, ⋯⟩
-- Mathlib.Algebra.Order.Field.Basic
div_le_iff_of_neg' : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α},
  c < 0 → (b / c ≤ a ↔ c * a ≤ b)
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHomClass.counitAlgHom_comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Bialgebra R A] [inst_3 : Semiring B] [inst_4 : Bialgebra R B] [inst_5 : FunLike F A B]
  [inst_6 : BialgHomClass F R A B] (f : F), (Bialgebra.counitAlgHom R B).comp ↑f = Bialgebra.counitAlgHom R A
-- Mathlib.CategoryTheory.Sites.Continuous
/-- A 1-hypercover in `C` is preserved by a functor `F : C ⥤ D` if the mapped 1-pre-hypercover
in `D` is a 1-hypercover for the given topology on `D`.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {X : C} → J.OneHypercover X → CategoryTheory.Functor C D → CategoryTheory.GrothendieckTopology D → Prop
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.postcomp_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  (E : Type u_4) {F : Type u_5} {G : Type u_6} [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : TopologicalSpace G]
  [inst_13 : IsTopologicalAddGroup F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜₃ G]
  [inst_16 : ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) (f : E →SL[σ] F), (ContinuousLinearMap.postcomp E L) f = L ∘SL f
-- Mathlib.Algebra.Star.CentroidHom
CentroidHom.starCenterIsoCentroid_symm_apply_coe : ∀ {α : Type u_1} [inst : NonAssocSemiring α] [inst_1 : StarRing α] (T : CentroidHom α),
  ↑(CentroidHom.starCenterIsoCentroid.symm T) = T 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- `CategoricalPullback.π₁ F G` is the first projection `CategoricalPullback F G ⥤ A`.  -/
CategoryTheory.Limits.CategoricalPullback.π₁ : {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) →
                CategoryTheory.Functor (CategoryTheory.Limits.CategoricalPullback F G) A
-- Mathlib.Data.Finset.Basic
Finset.erase_eq_empty_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (a : α), s.erase a = ∅ ↔ s = ∅ ∨ s = {a}
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instIsAddApply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N], IsAddApply (QuadraticMap R M N) M N
-- Lean.Data.PersistentArray
Lean.PersistentArray.modifyAux : {α : Type u} → [Inhabited α] → (α → α) → Lean.PersistentArrayNode α → USize → USize → Lean.PersistentArrayNode α
-- Mathlib.Topology.Piecewise
IsOpen.ite' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s s' t : Set α},
  IsOpen s → IsOpen s' → (∀ x ∈ frontier t, x ∈ s ↔ x ∈ s') → IsOpen (t.ite s s')
-- Init.Data.Array.Lemmas
List.toArray_drop : ∀ {α : Type u_1} {l : List α} {k : ℕ}, (List.drop k l).toArray = l.toArray.extract k
-- Mathlib.Data.Sum.Lattice
/-- `Sum.Lex.inrₗ` as a lattice homomorphism.  -/
Sum.Lex.inrLatticeHom : {α : Type u_1} → {β : Type u_2} → [inst : Lattice α] → [inst_1 : Lattice β] → LatticeHom β (α ⊕ₗ β)
-- Init.Data.List.MinMaxIdx
List.get_minIdxOn?_lt_length : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α}
  (h : (List.minIdxOn? f xs).isSome = true), (List.minIdxOn? f xs).get h < xs.length
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.finite_quotient_of_finite_quotient_of_finite_quotient : ∀ {G : Type u} {X : Type v} [inst : Group G] [inst_1 : MulAction G X] {H : Subgroup G}
  [Finite (MulAction.orbitRel.Quotient G X)] [Finite (G ⧸ H)], Finite (MulAction.orbitRel.Quotient (↥H) X)
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- **Alias** of `isCompact_setOfPred_probabilityMeasure_mass_eq_compl_isCompact_le`.

---

**Prokhorov theorem**: Given a sequence of compact sets `Kₙ` and a sequence `uₙ` tending to
zero, the probability measures giving mass at most `uₙ` to the complement of `Kₙ` form a
compact set.  -/
isCompact_setOf_probabilityMeasure_mass_eq_compl_isCompact_le : ∀ {E : Type u_1} [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  {u : ℕ → NNReal} {K : ℕ → Set E},
  Filter.Tendsto u Filter.atTop (nhds 0) →
    (∀ (n : ℕ), IsCompact (K n)) → NormalSpace E ∨ Monotone K → IsCompact {μ | ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
-- Mathlib.Order.Heyting.Basic
le_hnot_self : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a : α}, ￢a ≤ a ↔ a = ⊤
-- Init.Data.String.Basic
String.Pos.Raw.utf8PrevAux.eq_1 : ∀ (x x_1 : String.Pos.Raw), String.Pos.Raw.utf8PrevAux [] x x_1 = { byteIdx := x_1.byteIdx - 1 }
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
/-- A ring equivalence induces a uniform equivalence with respect to the adic topologies,
provided it preserves the defining ideals.  -/
WithIdeal.uniformEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : WithIdeal R] →
      {S : Type u_2} →
        [inst_2 : CommRing S] →
          [inst_3 : WithIdeal S] → (e : R ≃+* S) → Ideal.map e.toRingHom WithIdeal.i = WithIdeal.i → R ≃ᵤ S
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.lt_iff_exists : ∀ {α : Type u_1} [inst : LT α] {x y : WithZero α}, x < y ↔ ∃ b, y = ↑b ∧ ∀ (a : α), x = ↑a → a < b
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.bind' : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α β : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] {x : m α}
  {f : α → m β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond β ps},
  ⦃P⦄ x ⦃(fun a => (Std.Do.wp (f a)).apply Q, Q.2)⦄ → ⦃P⦄ (x >>= f) ⦃Q⦄
-- Mathlib.Algebra.Order.Floor.Ring
Int.mul_natCast_floor_div_cancel : ∀ {R : Type u_4} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] {n : ℕ},
  n ≠ 0 → ∀ (a : R), ⌊a * ↑n⌋ / ↑n = ⌊a⌋
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.supported_eq_range_rename : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R] (s : Set σ),
  MvPolynomial.supported R s = (MvPolynomial.rename Subtype.val).range
-- Mathlib.Order.PrimeIdeal
Order.PFilter.IsPrime.mk : ∀ {P : Type u_1} [inst : Preorder P] {F : Order.PFilter P}, Order.IsIdeal (↑F)ᶜ → F.IsPrime
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contStack.eq_5 : ∀ (c : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont),
  Turing.PartrecToTM2.contStack (Turing.ToPartrec.Cont.fix c k) = Turing.PartrecToTM2.contStack k
-- Mathlib.Order.ScottContinuity
ScottContinuousOn.sup₂ : ∀ {β : Type u_2} [inst : SemilatticeSup β] {D : Set (Set (β × β))},
  ScottContinuousOn D fun x =>
    match x with
    | (a, b) => a ⊔ b
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.lift_comp_swap : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P), (Monoid.Coprod.lift f g).comp (Monoid.Coprod.swap N M) = Monoid.Coprod.lift g f
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.mem_range_right : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d) (i : Fin (n + 1)), i ∈ Set.range ⇑(x.cast hd).simplex.2
-- Batteries.Data.List.Basic
List.takeListTR.eq_1 : ∀ {α : Type u_1} (xs : List α) (ns : List ℕ), xs.takeListTR ns = List.takeListTR.go ns xs #[]
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a `k`-linear `G`-representation `(A, ρ)` and a type `α`, this is the map
`(α →₀ A) →ₗ[k] (A ⊗ (α →₀ k[G]))_G` sending `single x a ↦ ⟦a ⊗ₜ single x 1⟧.`  -/
Rep.finsuppToCoinvariantsTensorFree : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        (α : Type u) → [DecidableEq α] → (α →₀ ↑A) →ₗ[k] (A.ρ.tprod (Rep.free k G α).ρ).Coinvariants
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- The proposition that a bilinear form is reflexive  -/
LinearMap.BilinForm.IsRefl : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.BilinForm R M → Prop
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.directive.guardOpenerSize : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Lean.Meta.Sym.Arith.Poly
/-- `sharesVar m₁ m₂` returns `true` if `m₁` and `m₂` shares at least one variable.  -/
Lean.Grind.CommRing.Mon.sharesVar : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Bool
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.mul_Nonneg : ∀ (p : Lean.Grind.Linarith.Poly) (k : ℕ), p.NonnegCoeffs → (p.mul ↑k).NonnegCoeffs
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- Updates the current state with a new max variable and comparisons,
and calls `validate` to check for a contradiction.
 -/
Mathlib.Tactic.Linarith.update : ℕ → Mathlib.Tactic.Linarith.PCompSet → Mathlib.Tactic.Linarith.LinarithM Unit
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trNormal.eq_3 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (dec : List.Vector Bool n → Γ) (a : Γ → σ → σ)
  (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to1.trNormal dec (Turing.TM1.Stmt.load a q) =
    Turing.TM1to1.read dec fun a_1 => Turing.TM1.Stmt.load (fun x s => a a_1 s) (Turing.TM1to1.trNormal dec q)
-- Mathlib.Algebra.Ring.Defs
/-- A typeclass stating that multiplication is left distributive over addition.  -/
LeftDistribClass : (R : Type u_1) → [Mul R] → [Add R] → Prop
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instWeaklyLocallyCompactSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [WeaklyLocallyCompactSpace M], WeaklyLocallyCompactSpace Mᵈᵃᵃ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Adj.length_toWalk : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), h.toWalk.length = 1
-- Init.Data.UInt.BasicAux
/-- Adds two 32-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.add : UInt32 → UInt32 → UInt32
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_nonneg_iff : ∀ {x : ℝ}, 0 < x → (0 ≤ Real.log x ↔ 1 ≤ x)
-- Lean.Class
/-- Class name.  -/
Lean.ClassEntry.name : Lean.ClassEntry → Lean.Name
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The functor `HomologicalComplex C c ⥤ ShortComplex C` which sends a homological
complex `K` to the short complex `K.X i ⟶ K.X j ⟶ K.X k` for arbitrary indices `i`, `j` and `k`.  -/
HomologicalComplex.shortComplexFunctor' : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        (c : ComplexShape ι) →
          ι → ι → ι → CategoryTheory.Functor (HomologicalComplex C c) (CategoryTheory.ShortComplex C)
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.instMonoidalLinearFullSubcategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] [inst_3 : CategoryTheory.Preadditive C] (R : Type u_1)
  [inst_4 : Ring R] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.MonoidalPreadditive C]
  [CategoryTheory.MonoidalLinear R C], CategoryTheory.MonoidalLinear R P.FullSubcategory
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to `EReal`. The unprimed version of
the lemma uses `[ContinuousAdd]`.  -/
LowerSemicontinuous.add' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_5} [inst_1 : AddCommMonoid γ] [inst_2 : LinearOrder γ]
  [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] {f g : α → γ},
  LowerSemicontinuous f →
    LowerSemicontinuous g →
      (∀ (x : α), ContinuousAt (fun p => p.1 + p.2) (f x, g x)) → LowerSemicontinuous fun z => f z + g z
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.ofInv_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (s : Y ⟶ X) (hs : W s), (CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).s = s
-- Lean.Meta.Match.Match
/-- If constraint is of the form `e ≋ x` where `x` is a free variable, reorient it
as `x ≋ e` If
- `x` is an `alt`-local declaration
- `e` is not a free variable.
 -/
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.reorientCnstrs : Lean.Meta.Match.Alt → Lean.Meta.Match.Alt
-- Mathlib.Topology.Irreducible
Subtype.irreducibleSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsIrreducible s → IrreducibleSpace ↑s
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.coeff_toAdicCompletionInv : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] {x : σ →₀ ℕ}
  {f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)},
  (MvPowerSeries.coeff x) (MvPowerSeries.toAdicCompletionInv σ R f) =
    MvPolynomial.coeff x (Quotient.out (↑f (Finsupp.degree x + 1)))
-- Mathlib.MeasureTheory.Measure.Prod
/-- `μ.prod ν` has finite spanning sets in rectangles of finite spanning sets.  -/
MeasureTheory.Measure.FiniteSpanningSetsIn.prod : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] →
        {μ : MeasureTheory.Measure α} →
          {ν : MeasureTheory.Measure β} →
            {C : Set (Set α)} →
              {D : Set (Set β)} →
                μ.FiniteSpanningSetsIn C →
                  ν.FiniteSpanningSetsIn D → (μ.prod ν).FiniteSpanningSetsIn (Set.image2 (fun x1 x2 => x1 ×ˢ x2) C D)
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.solverExtensionsRef : IO.Ref (Array (Lean.Meta.Grind.SolverExtension Lean.Meta.Grind.SolverExtensionState))
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.inv : ∀ {n : Type u_2} {R' : Type u_4} [inst : CommRing R'] [inst_1 : PartialOrder R'] [inst_2 : StarRing R']
  [inst_3 : Fintype n] [inst_4 : DecidableEq n] {M : Matrix n n R'}, M.PosSemidef → M⁻¹.PosSemidef