mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.instIsScalarTowerRing : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) {R₀ : Type u_1} [inst_3 : CommRing R₀] [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S]
  [IsScalarTower R₀ R S], IsScalarTower R₀ P.Ring S
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentEdit.textDocument : Lean.Lsp.TextDocumentEdit → Lean.Lsp.VersionedTextDocumentIdentifier
-- Mathlib.Topology.Closure
IsClosed.closure_subset_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsClosed t → (closure s ⊆ t ↔ s ⊆ t)
-- Mathlib.Control.Monad.Cont
WriterT.mkLabel' : {m : Type u → Type v} →
  [Monad m] →
    {α : Type u_1} → {β ω : Type u} → [Monoid ω] → MonadCont.Label (α × ω) m β → MonadCont.Label α (WriterT ω m) β
-- Lean.Parser.Term
Lean.Parser.Term.trailing_parser.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Iter.forIn'_eq_match_step.match_1.eq_1 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.yield c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_1 c
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- Positive part of the Jordan decomposition  -/
MeasureTheory.JordanDecomposition.posPart : {α : Type u_2} → [inst : MeasurableSpace α] → MeasureTheory.JordanDecomposition α → MeasureTheory.Measure α
-- Lean.Meta.MonadSimp
Lean.Meta.MonadSimp.Result.step.inj : ∀ {e h e_1 h_1 : Lean.Expr},
  Lean.Meta.MonadSimp.Result.step e h = Lean.Meta.MonadSimp.Result.step e_1 h_1 → e = e_1 ∧ h = h_1
-- Mathlib.Order.Filter.Bases.Basic
Filter.IsBasis.hasBasis : ∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s), h.filter.HasBasis p s
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- The setoid defined by the `SameCycle` relation.  -/
Equiv.Perm.SameCycle.setoid : {α : Type u_2} → Equiv.Perm α → Setoid α
-- Mathlib.CategoryTheory.Equivalence
/-- An equivalence of categories.

We define an equivalence between `C` and `D`, with notation `C ≌ D`, as a half-adjoint equivalence:
a pair of functors `F : C ⥤ D` and `G : D ⥤ C` with a unit `η : 𝟭 C ≅ F ⋙ G` and counit
`ε : G ⋙ F ≅ 𝟭 D`, such that the natural isomorphisms `η` and `ε` satisfy the triangle law for
`F`: namely, `Fη ≫ εF = 𝟙 F`. Or, in other words, the composite `F` ⟶ `F ⋙ G ⋙ F` ⟶ `F` is the
identity.

In `unit_inverse_comp`, we show that this is sufficient to establish a full adjoint
equivalence. I.e., the composite `G` ⟶ `G ⋙ F ⋙ G` ⟶ `G` is also the identity.

The triangle equation `functor_unitIso_comp` is written as a family of equalities between
morphisms. It is more complicated if we write it as an equality of natural transformations, because
then we would either have to insert natural transformations like `F ⟶ F𝟭` or abuse defeq.  -/
CategoryTheory.«term_≌_» : Lean.TrailingParserDescr
-- Mathlib.Topology.DenseEmbedding
IsDenseEmbedding.dense_image : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {e : α → β},
  IsDenseEmbedding e → ∀ {s : Set α}, Dense (e '' s) ↔ Dense s
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algEquivCMulXAddC_symm_eq : ∀ {R : Type u_3} [inst : CommRing R] (a b : R) [inst_1 : Invertible a],
  (Polynomial.algEquivCMulXAddC a b).symm = Polynomial.algEquivCMulXAddC (⅟a) (-⅟a * b)
-- Mathlib.Data.List.Basic
List.eq_replicate_length : ∀ {α : Type u} {a : α} {l : List α}, l = List.replicate l.length a ↔ ∀ b ∈ l, b = a
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instPowInt32SintOfNatNat : Lean.Grind.ToInt.Pow Int32 (Lean.Grind.IntInterval.sint 32)
-- Mathlib.Topology.Order.IntermediateValue
IsPreconnected.intermediate_value₂_eventually₁ : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] {s : Set X},
  IsPreconnected s →
    ∀ {a : X} {l : Filter X},
      a ∈ s →
        ∀ [l.NeBot],
          l ≤ Filter.principal s →
            ∀ {f g : X → α}, ContinuousOn f s → ContinuousOn g s → f a ≤ g a → g ≤ᶠ[l] f → ∃ x ∈ s, f x = g x
-- Mathlib.Topology.MetricSpace.Defs
MetricSpace.ext_iff : ∀ {α : Type u_3} {m m' : MetricSpace α}, m = m' ↔ m.toDist = m'.toDist
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instIsIsoSchemeSigmaSpecOfFinite : ∀ {ι : Type u} [Finite ι] (R : ι → CommRingCat), CategoryTheory.IsIso (AlgebraicGeometry.sigmaSpec R)
-- Mathlib.Order.RelSeries
/-- A relation `r` is said to be infinite dimensional iff there exists relation series of arbitrary
length.  -/
SetRel.InfiniteDimensional : {α : Type u_1} → SetRel α α → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.toLinearOrderMultispanIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w}
  (I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C) [inst_1 : LinearOrder ι]
  (X : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι)),
  I.toLinearOrderMultispanIso.inv.app X =
    (match X with
      | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.Iso.refl (I.left ↑a)
      | CategoryTheory.Limits.WalkingMultispan.right a => CategoryTheory.Iso.refl (I.right a)).inv
-- Mathlib.Algebra.Module.Submodule.Equiv
/-- The top submodule of `M` is linearly equivalent to `M`.  -/
LinearEquiv.ofTop : {R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → {module_M : Module R M} → (p : Submodule R M) → p = ⊤ → ↥p ≃ₗ[R] M
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.ofAddUnits_sup_addUnits : ∀ {M : Type u_1} [inst : AddMonoid M] (S T : AddSubgroup (AddUnits M)), (S.ofAddUnits ⊔ T.ofAddUnits).addUnits = S ⊔ T
-- Init.Data.String.Lemmas.Pattern.Basic
_private.Init.Data.String.Lemmas.Pattern.Basic.0.String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.instIteratorIdSearchStepOfForwardPattern.match_3.splitter : {ρ : Type} →
  (pat : ρ) →
    (s : String.Slice) →
      (it : Std.IterM Id (String.Slice.Pattern.SearchStep s)) →
        (motive : Option (s.sliceFrom it.internalState.currPos).Pos → Sort u_1) →
          (x : Option (s.sliceFrom it.internalState.currPos).Pos) →
            ((pos : (s.sliceFrom it.internalState.currPos).Pos) → x = some pos → motive (some pos)) →
              (x = none → motive none) → motive x
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_mul_X_eq_monomial : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {s : σ} {a : R},
  MvPolynomial.C a * MvPolynomial.X s = (MvPolynomial.monomial fun₀ | s => 1) a
-- Init.Data.Option.Lemmas
Option.min_eq_right_of_lt : ∀ {α : Type u_1} [inst : LT α] [inst_1 : Min α],
  (∀ (x y : α), y < x → x ⊓ y = y) → ∀ {a b : Option α}, b < a → a ⊓ b = b
-- Mathlib.Order.IsNormal
Order.IsNormal.id : ∀ {α : Type u_1} [inst : LinearOrder α], Order.IsNormal id
-- Mathlib.Logic.Embedding.Basic
/-- Embedding into `Option α` using `some`.  -/
Function.Embedding.some : {α : Type u_1} → α ↪ Option α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.iteratedDeriv_add_one_sin : ∀ (n : ℕ), iteratedDeriv (n + 1) Real.sin = iteratedDeriv n Real.cos
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
/-- If a precoverage satisfies `HasIsos`, `IsStableUnderBaseChange` and
`IsStableUnderComposition` (which is a slightly stronger condition as compared
to pretopologies), then in order to check that a pseudofunctor is a prestack
it suffices to check that it is a prestack for the presieves that are
part of the precoverage.  -/
CategoryTheory.Pseudofunctor.IsPrestack.of_precoverage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.Precoverage C} [J.HasIsos] [J.IsStableUnderBaseChange]
  [J.IsStableUnderComposition], (∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R) → F.IsPrestack J.toGrothendieck
-- Init.Data.SInt.Lemmas
ISize.toBitVec_maxValue : ISize.maxValue.toBitVec = BitVec.intMax System.Platform.numBits
-- Mathlib.Order.Heyting.Hom
OrderIsoClass.toCoheytingHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : CoheytingAlgebra α]
  {x : CoheytingAlgebra β} [OrderIsoClass F α β], CoheytingHomClass F α β
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.epi_kernelLift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [S.HasHomology] [inst_3 : CategoryTheory.Limits.HasKernel S.g],
  S.Exact → CategoryTheory.Epi (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)
-- Mathlib.CategoryTheory.Limits.EpiMono
CategoryTheory.mono_iff_isPullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Mono f ↔
    CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X) f f
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.centralizer_toSubsemigroup : ∀ {M : Type u_1} (S : Set M) [inst : Monoid M], (Submonoid.centralizer S).toSubsemigroup = Subsemigroup.centralizer S
-- Mathlib.Topology.List
nhds_nil : ∀ {α : Type u_1} [inst : TopologicalSpace α], nhds [] = pure []
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.map : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [BorelSpace α] [inst_3 : MeasurableSpace β] [inst_4 : TopologicalSpace β] [BorelSpace β] [μ.InnerRegular]
  (f : α ≃ₜ β), (MeasureTheory.Measure.map (⇑f) μ).InnerRegular
-- Mathlib.NumberTheory.Dioph
Poly.instMul : {α : Type u_1} → Mul (Poly α)
-- Mathlib.Data.ZMod.Basic
ZMod.inv_coe_unit : ∀ {n : ℕ} (u : (ZMod n)ˣ), (↑u)⁻¹ = ↑u⁻¹
-- Mathlib.Topology.Sheaves.Skyscraper
/-- On an open set not containing `p₀`, the value of skyscraper sheaf supported at `p₀` is a terminal
object.
 -/
isTerminalSkyscraperSheafObjObjOfNotMem : {X : TopCat} →
  {p₀ : ↑X} →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          {A : C} →
            [inst_2 : CategoryTheory.Limits.HasTerminal C] →
              {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} →
                p₀ ∉ Opposite.unop U → CategoryTheory.Limits.IsTerminal ((skyscraperSheaf p₀ A).obj.obj U)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_diff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)], (m₁ \ m₂).get! k = if k ∈ m₂ then default else m₁.get! k
-- Mathlib.Logic.Function.Iterate
Function.Commute.iterate_right : ∀ {α : Type u} {f g : α → α}, Function.Commute f g → ∀ (n : ℕ), Function.Commute f g^[n]
-- ProofWidgets.Data.Html
/-- Interpolates a collection into a JSX attribute literal.
For HTML tags, this should have type `Array (String × Json)`.
For `ProofWidgets.Component`s, it can be any structure `$t` whatsoever:
it is interpolated into the component's props using `{ $t with ... }` notation.  -/
ProofWidgets.Jsx.«proofWidgetsJsxAttr{..._}» : Lean.ParserDescr
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_punit : Cardinal.mk PUnit.{u_1 + 1} = 1
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.shareCommonPreDefs : Array Lean.Elab.PreDefinition → Lean.CoreM (Array Lean.Elab.PreDefinition)
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.prod : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} {ι' : Type u_5} {s : Set ι} {t : Set ι'} {f : ι → Set α}
  {g : ι' → Set β}, s.PairwiseDisjoint f → t.PairwiseDisjoint g → (s ×ˢ t).PairwiseDisjoint fun i => f i.1 ×ˢ g i.2
-- Mathlib.Tactic.Basic
/-- Info trees produced by the executed tactic, wrapped in `CommandContextInfo.save`.  -/
Mathlib.Tactic.withResetServerInfo.Result.trees : {α : Type} → Mathlib.Tactic.withResetServerInfo.Result α → Lean.PersistentArray Lean.Elab.InfoTree
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange_add : ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → AddZeroClass (β₁ i)]
  [inst_1 : (i : ι) → AddZeroClass (β₂ i)] (f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0),
  (∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y) →
    ∀ (g₁ g₂ : Π₀ (i : ι), β₁ i),
      DFinsupp.mapRange f hf (g₁ + g₂) = DFinsupp.mapRange f hf g₁ + DFinsupp.mapRange f hf g₂
-- Lean.Data.Json.FromToJson.Basic
/-- Types that can be decoded from JSON.

Use `deriving FromJson`
to [automatically generate](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=deriving-instances) an instance.
See `ToJson`
for details of auto-generated instances.
 -/
Lean.FromJson : Type u → Type u
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- It is the unique such map to do this  -/
CategoryTheory.Limits.IsLimit.uniq : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (self : CategoryTheory.Limits.IsLimit t)
  (s : CategoryTheory.Limits.Cone F) (m : s.pt ⟶ t.pt),
  (∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) → m = self.lift s
-- Mathlib.GroupTheory.Descent
/-- If `G` is a commutative additive group and `n : ℕ`, `h : G → ℝ` satisfy
* for all `x : G`, `h (n • x) ≥ b * h x - c₀`,
* for all `B : ℝ`, there are only finitely many `x : G` such that `h x ≤ B`,

where `1 < b` and `c₀` are real numbers, then the torsion subgroup of `G` is finite.  -/
AddCommGroup.finite_torsion_of_descent : ∀ {G : Type u_1} [inst : AddCommGroup G] {n : ℕ} {h : G → ℝ} {b c₀ : ℝ},
  1 < b → (∀ (x : G), b * h x - c₀ ≤ h (n • x)) → ∀ [Northcott h], Finite ↥(AddCommGroup.torsion G)
-- Mathlib.Order.UpperLower.Closure
UpperSet.lt_sdiff_left : ∀ {α : Type u_1} [inst : Preorder α] {s : UpperSet α} {t : Set α}, s < s.sdiff t ↔ ¬Disjoint (↑s) t
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_fin_succ_eq_det_submatrix : ∀ {α : Type w} [inst : CommRing α] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) α) (i j : Fin n.succ),
  A.adjugate i j = (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Origin.decl.inj : ∀ {declName declName_1 : Lean.Name},
  Lean.Meta.Grind.Origin.decl declName = Lean.Meta.Grind.Origin.decl declName_1 → declName = declName_1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesImage.iso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasCokernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))],
  CategoryTheory.Abelian.PreservesImage.iso F f = CategoryTheory.Abelian.PreservesImage.iso F f
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `mul_lt_mul_of_nonneg_of_pos'`.

---

**Alias** of `mul_lt_mul_of_le_of_lt_of_nonneg_of_pos`. -/
mul_lt_mul' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulStrictMono α]
  [MulPosMono α], a ≤ b → c < d → 0 ≤ c → 0 < b → a * c < b * d
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.M.mk_eq : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) (x y : (j : J) × ↑(F.obj j)),
  (∃ k f g,
      (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd = (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd) →
    ModuleCat.FilteredColimits.M.mk F x = ModuleCat.FilteredColimits.M.mk F y
-- Mathlib.Order.Part
Monotone.partBind : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] {f : α → Part β} {g : α → β → Part γ},
  Monotone f → Monotone g → Monotone fun x => (f x).bind (g x)
-- Init.System.IO
/-- Pauses execution for the specified number of milliseconds.
 -/
IO.sleep : UInt32 → BaseIO Unit
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.commGroup : {α : Type u} → [AddCommGroup α] → CommGroup (Multiplicative α)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.oreSubVAddChar'.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] (r₁ : R) (r₂ : X) (s₁ s₂ : ↥S),
  AddOreLocalization.oreSubVAddChar' r₁ r₂ s₁ s₂ =
    ⟨AddOreLocalization.oreMin r₁ s₂, ⟨AddOreLocalization.oreSubtra r₁ s₂, ⋯⟩⟩
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.SupportsStmt.match_1.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4) (a : Γ → σ → Γ)
  (q : Turing.TM1.Stmt Γ Λ σ) (h_1 : (a : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.move a q))
  (h_2 : (a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.write a q))
  (h_3 : (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.load a q))
  (h_4 : (a : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.branch a q₁ q₂))
  (h_5 : (l : Γ → σ → Λ) → motive (Turing.TM1.Stmt.goto l)) (h_6 : Unit → motive Turing.TM1.Stmt.halt),
  (match Turing.TM1.Stmt.write a q with
    | Turing.TM1.Stmt.move a q => h_1 a q
    | Turing.TM1.Stmt.write a q => h_2 a q
    | Turing.TM1.Stmt.load a q => h_3 a q
    | Turing.TM1.Stmt.branch a q₁ q₂ => h_4 a q₁ q₂
    | Turing.TM1.Stmt.goto l => h_5 l
    | Turing.TM1.Stmt.halt => h_6 ()) =
    h_2 a q
-- Mathlib.Order.Grade
grade_mono : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : PartialOrder α] [inst_2 : GradeOrder 𝕆 α],
  Monotone (grade 𝕆)
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.swap_obj_toTwoPointing : ∀ (X : TwoP), (TwoP.swap.obj X).toTwoPointing = X.toTwoPointing.swap
-- Mathlib.Analysis.RCLike.Inner
RCLike.linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero : ∀ {ι : Type u_1} {κ : Type u_2} {𝕜 : Type u_3} [inst : Fintype ι] [inst_1 : RCLike 𝕜] {f : κ → ι → 𝕜},
  (∀ (k : κ), f k ≠ 0) → (Pairwise fun k₁ k₂ => ⟪f k₁, f k₂⟫ₙ_[𝕜] = 0) → LinearIndependent 𝕜 f
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_sum_right : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] [StarModule ℂ A] {ι : Type u_3} {s : Finset ι} {x : E} {y : ι → E},
  inner A x (∑ i ∈ s, y i) = ∑ i ∈ s, inner A x (y i)
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.findFinIdx?.go.match_1.eq_2 : ∀ {α : Type u_1} (l : List α) (motive : (x : List α) → (x_1 : ℕ) → x.length + x_1 = l.length → Sort u_2) (a : α)
  (l_1 : List α) (i : ℕ) (h : (a :: l_1).length + i = l.length)
  (h_1 : (x : ℕ) → (x_1 : [].length + x = l.length) → motive [] x x_1)
  (h_2 : (a : α) → (l_2 : List α) → (i : ℕ) → (h : (a :: l_2).length + i = l.length) → motive (a :: l_2) i h),
  (match a :: l_1, i, h with
    | [], x, x_1 => h_1 x x_1
    | a :: l_2, i, h => h_2 a l_2 i h) =
    h_2 a l_1 i h
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.MkHInjTypeResult.mk.injEq : ∀ (thmType : Lean.Expr) (us : List Lean.Level) (numIndices : ℕ) (thmType_1 : Lean.Expr) (us_1 : List Lean.Level)
  (numIndices_1 : ℕ),
  ({ thmType := thmType, us := us, numIndices := numIndices } =
      { thmType := thmType_1, us := us_1, numIndices := numIndices_1 }) =
    (thmType = thmType_1 ∧ us = us_1 ∧ numIndices = numIndices_1)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Filter.Eventually.volume_pos_of_nhds_real : ∀ {p : ℝ → Prop} {a : ℝ}, (∀ᶠ (x : ℝ) in nhds a, p x) → 0 < MeasureTheory.volume {x | p x}
-- Lean.Meta.Tactic.Injection
Lean.Meta.injection : Lean.MVarId → Lean.FVarId → optParam (List Lean.Name) [] → Lean.MetaM Lean.Meta.InjectionResult
-- Mathlib.Data.Sign.Defs
instInhabitedSignType : Inhabited SignType
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
/-- Two-sided-ideals of `A` and that of `Aᵒᵖ` corresponds bijectively to each other.
 -/
TwoSidedIdeal.opOrderIso : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → TwoSidedIdeal R ≃o TwoSidedIdeal Rᵐᵒᵖ
-- Mathlib.Algebra.Tropical.Basic
Tropical.add_self : ∀ {R : Type u} [inst : LinearOrder R] (x : Tropical R), x + x = x
-- Mathlib.Order.Basic
/-- To prove commutativity of a binary operation `○`, we only to check `a ○ b ≤ b ○ a` for all `a`,
`b`.  -/
commutative_of_le : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] {f : β → β → α},
  (∀ (a b : β), f a b ≤ f b a) → ∀ (a b : β), f a b = f b a
-- Lean.Widget.InteractiveGoal
/-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity.  -/
Lean.Widget.goalToInteractive : Lean.MVarId → Lean.MetaM Lean.Widget.InteractiveGoal
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f] (U : Y.Opens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.preimageIso f U).hom U.ι =
    CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι f
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  (f : α → C) (x : CategoryTheory.IsFiltered.FilteredClosureSmall.AbstractFilteredClosure✝ f),
  CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization✝ f x =
    (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure✝ f x.fst).snd x.snd
-- Lean.Util.PPExt
Lean.PPFns.ppTerm : Lean.PPFns → Lean.PPContext → Lean.Term → IO Std.Format
-- Lean.Data.PrefixTree
Lean.PrefixTree.insert : {α : Type u_1} → {β : Type u_2} → {p : α → α → Ordering} → Lean.PrefixTree α β p → List α → β → Lean.PrefixTree α β p
-- Mathlib.Analysis.Normed.Group.Basic
SeminormedGroup.disjoint_nhds_one : ∀ {E : Type u_5} [inst : SeminormedGroup E] (f : Filter E), Disjoint (nhds 1) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y‖
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- Given an adjunction `L ⊣ R`, if `L ⋙ R` is abstractly isomorphic to the identity functor, then the
unit is an isomorphism.
 -/
CategoryTheory.Adjunction.unitAsIsoOfIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor D C} →
            (L ⊣ R) → (L.comp R ≅ CategoryTheory.Functor.id C) → (CategoryTheory.Functor.id C ≅ L.comp R)
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- The bicategory structure on `BasedCategory.{v₂, u₂} 𝒮` is strict.  -/
CategoryTheory.BasedCategory.instStrict : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮],
  CategoryTheory.Bicategory.Strict (CategoryTheory.BasedCategory 𝒮)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {v : β k}, t.get? k = some v ↔ ∃ (h : k ∈ t), t.get k h = v