mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Quantale
/-- A quantale is a semigroup distributing over a complete lattice.  -/
AddQuantale : (α : Type u_1) → [inst : AddSemigroup α] → [inst_1 : CompleteLattice α] → [IsAddQuantale α] → Type
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionDisabled.mk : String → Lean.Lsp.CodeActionDisabled
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.rightInverseUnitor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.prod.rightInverseUnitor C).obj X = (X, { as := PUnit.unit })
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.specializes_iff_of_t1Space : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} [T1Space α], s ⤳ t ↔ s ⊆ t ∧ t ⊆ closure s
-- Init.Core
ForInStep.done.inj : ∀ {α : Type u} {a a_1 : α}, ForInStep.done a = ForInStep.done a_1 → a = a_1
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
CliffordAlgebra.toBaseChange_comp_ofBaseChange : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
  [inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V),
  (CliffordAlgebra.toBaseChange A Q).comp (CliffordAlgebra.ofBaseChange A Q) =
    AlgHom.id A (TensorProduct R A (CliffordAlgebra Q))
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.hasColimit_of_hasColimitπ : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
  [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)]
  [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)]
  [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)], CategoryTheory.Limits.HasColimit F
-- Lean.Setup
Lean.instInhabitedImportArtifacts.default : Lean.ImportArtifacts
-- Mathlib.Combinatorics.Configuration
Configuration.ofField.eq_or_eq_of_orthogonal : ∀ {K : Type u_3} [inst : Field K] {a b c d : Projectivization K (Fin 3 → K)},
  a.orthogonal c → b.orthogonal c → a.orthogonal d → b.orthogonal d → a = b ∨ c = d
-- Mathlib.Topology.Algebra.Module.Equiv
/-- See Note [custom simps projection]  -/
ContinuousLinearEquiv.Simps.symm_apply : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {σ₂₁ : R₂ →+* R₁} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                {M₁ : Type u_4} →
                  [inst_4 : TopologicalSpace M₁] →
                    [inst_5 : AddCommMonoid M₁] →
                      {M₂ : Type u_5} →
                        [inst_6 : TopologicalSpace M₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R₁ M₁] → [inst_9 : Module R₂ M₂] → (M₁ ≃SL[σ₁₂] M₂) → M₂ → M₁
-- Lean.ResolveName
Lean.ResolveName.backward.privateInPublic.warn : Lean.Option Bool
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_finsetSum : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} (s : Finset ι) (p : ι → Polynomial R) (n : ℕ),
  (∑ i ∈ s, p i).homogenize n = ∑ i ∈ s, (p i).homogenize n
-- Lean.Expr
Lean.mkApp10 : Lean.Expr →
  Lean.Expr →
    Lean.Expr →
      Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Order.Bounds.OrderIso
OrderIso.isGLB_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set α} {x : β},
  IsGLB (⇑f '' s) x ↔ IsGLB s (f.symm x)
-- Mathlib.RingTheory.Coalgebra.Convolution
LinearMap.instIsScalarTowerWithConvId : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {C : Type u_5} [inst : CommSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A] [inst_3 : SMulCommClass R A A]
  [inst_4 : IsScalarTower R A A] [inst_5 : AddCommMonoid C] [inst_6 : Module R C] [inst_7 : CoalgebraStruct R C]
  [inst_8 : Monoid S] [inst_9 : DistribMulAction S A] [inst_10 : SMulCommClass R S A] [IsScalarTower S A A],
  IsScalarTower S (WithConv (C →ₗ[R] A)) (WithConv (C →ₗ[R] A))
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.equivOfIsoObj_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type w)} {X Y : C}
  (e : Y ≅ X) (R : F.CorepresentableBy X), (CategoryTheory.Functor.CorepresentableBy.equivOfIsoObj e) R = R.ofIsoObj e
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_cancel' : ∀ {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] (m : M) (s : ↥S), s • IsLocalizedModule.mk' f m s = f m
-- Mathlib.Analysis.Calculus.FDeriv.Pow
fderivWithin_pow_ring : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {s : Set 𝔸} {x : 𝔸} (n : ℕ),
  UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (fun x => x ^ n) s x = (n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.equiv_mkInv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [inst_2 : L.IsLocalization W] {X Y : C}
  (f : Y ⟶ X) (hf : W f) [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y],
  (CategoryTheory.Localization.SmallHom.equiv W L) (CategoryTheory.Localization.SmallHom.mkInv f hf) =
    (CategoryTheory.Localization.isoOfHom L W f hf).inv
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.foldlM.eq_2 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [inst : Monad m] (f : δ → (a : α) → β a → m δ)
  (init : δ) (size : ℕ) (k' : α) (v : β k') (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.foldlM f init (Std.DTreeMap.Internal.Impl.inner size k' v l r) = do
    let left ← Std.DTreeMap.Internal.Impl.foldlM f init l
    let middle ← f left k' v
    Std.DTreeMap.Internal.Impl.foldlM f middle r
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- The actual `NonUnitalSubsemiring` obtained from an element of a `NonUnitalSubsemiringClass`.  -/
NonUnitalSubsemiring.ofClass : {S : Type u_1} →
  {R : Type u_2} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : SetLike S R] → [NonUnitalSubsemiringClass S R] → S → NonUnitalSubsemiring R
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.image_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' F'' : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F) (f : F ⟶ F') (g : F' ⟶ F''),
  G.image (CategoryTheory.CategoryStruct.comp f g) = (G.image f).image g
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opEquivalence_unitIso : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V],
  (HomologicalComplex.opEquivalence V c).unitIso = HomologicalComplex.opUnitIso V c
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldl_loop_eq : ∀ {α : Sort u_1} {n : ℕ} (f : α → Fin n → α) (x : α), Fin.foldl.loop n f x n = x
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {X Y : CategoryTheory.Sheaf J A},
  (CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.app (Opposite.op X)).app Y =
    CategoryTheory.Sheaf.homEquiv.symm.toIso
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramProps.mk.injEq : ∀ (embeds : Array (String × ProofWidgets.Html)) (dsl sty sub : String) (maxOptSteps : ℕ)
  (embeds_1 : Array (String × ProofWidgets.Html)) (dsl_1 sty_1 sub_1 : String) (maxOptSteps_1 : ℕ),
  ({ embeds := embeds, dsl := dsl, sty := sty, sub := sub, maxOptSteps := maxOptSteps } =
      { embeds := embeds_1, dsl := dsl_1, sty := sty_1, sub := sub_1, maxOptSteps := maxOptSteps_1 }) =
    (embeds = embeds_1 ∧ dsl = dsl_1 ∧ sty = sty_1 ∧ sub = sub_1 ∧ maxOptSteps = maxOptSteps_1)
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.congr_eq_3 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1)
  (step : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n)) (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))) (id : ℕ)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array ℕ),
  step = some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) →
    (match step with
      | none => h_1 ()
      | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
      | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
      | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
      | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) ≍
      h_3 id c rupHints
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.unitOfList_eq_insertManyIfNewUnit : ∀ {α : Type u} {instOrd : Ord α} {l : List α},
  Std.DTreeMap.Internal.Impl.Const.unitOfList l =
    ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_mem_multiset : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (m : Multiset ι) (f : { x // x ∈ m } → M)
  (g : ι → M), (∀ (x : { x // x ∈ m }), f x = g ↑x) → ∏ x, f x = ∏ x ∈ m.toFinset, g x
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.toMonoidHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (h : M ≃* N),
  h.toMonoidHom = { toFun := h.toFun, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Presentable.StrongGenerator
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P P_1 : CategoryTheory.ObjectProperty C),
  P = P_1 →
    ∀ (κ κ_1 : Cardinal.{w}) (e_κ : κ = κ_1) [inst_1 : Fact κ.IsRegular],
      P.IsCardinalFilteredGenerator κ = P_1.IsCardinalFilteredGenerator κ_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.negMap_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  W.Nonsingular P → P 2 = 0 → W.negMap ⟦P⟧ = ⟦![1, 1, 0]⟧
-- Mathlib.Analysis.Matrix.Spectrum
/-- The eigenvalues of a Hermitian matrix, indexed by `Fin (Fintype.card n)` where `n` is the index
type of the matrix.  -/
Matrix.IsHermitian.eigenvalues₀ : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {n : Type u_2} →
      [inst_1 : Fintype n] → {A : Matrix n n 𝕜} → [DecidableEq n] → A.IsHermitian → Fin (Fintype.card n) → ℝ
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonDidChangeTextDocumentParams : Lean.FromJson Lean.Lsp.DidChangeTextDocumentParams
-- Mathlib.Topology.EMetricSpace.Defs
edist_pos : ∀ {γ : Type w} [inst : EMetricSpace γ] {x y : γ}, 0 < edist x y ↔ x ≠ y
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
/-- The product over a sigma type equals the product of the fiberwise products.
For rewriting in the reverse direction, use `Finset.prod_sigma'`.

See also `Fintype.prod_sigma` for the product over the whole type.  -/
Finset.prod_sigma : ∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a))
  (f : Sigma σ → β), ∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩
-- Mathlib.Algebra.Ring.BooleanRing
/-- Multiplication in a Boolean ring is idempotent.  -/
BooleanRing.isIdempotentElem : ∀ {α : Type u_4} [self : BooleanRing α] (a : α), IsIdempotentElem a
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUTimes.idle : Std.Internal.UV.System.CPUTimes → UInt64
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry?.induct : ∀ {α : Type u} {β : α → Type v} (motive : Std.DTreeMap.Internal.Impl α β → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf →
    (∀ (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r)) →
      (∀ (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) →
            motive
              (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)) →
        ∀ (a : Std.DTreeMap.Internal.Impl α β), motive a
-- Mathlib.RingTheory.Flat.Equalizer
/-- The bilinear map corresponding to `LinearMap.tensorEqLocus`.  -/
LinearMap.tensorEqLocusBil : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    {N : Type u_4} →
                      {P : Type u_5} →
                        [inst_7 : AddCommGroup N] →
                          [inst_8 : AddCommGroup P] →
                            [inst_9 : Module R N] →
                              [inst_10 : Module R P] →
                                (f g : N →ₗ[R] P) →
                                  M →ₗ[S]
                                    ↥(f.eqLocus g) →ₗ[R]
                                      ↥(((TensorProduct.AlgebraTensorModule.lTensor S M) f).eqLocus
                                          ((TensorProduct.AlgebraTensorModule.lTensor S M) g))
-- Lean.Server.Requests
Lean.Server.StatefulRequestHandler.mk.injEq : ∀ (fileSource : Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri)
  (pureHandle : Lean.Json → Dynamic → Lean.Server.RequestM (Lean.Server.SerializedLspResponse × Dynamic))
  (handle : Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse))
  (pureOnDidChange : Lean.Lsp.DidChangeTextDocumentParams → StateT Dynamic Lean.Server.RequestM Unit)
  (onDidChange : Lean.Lsp.DidChangeTextDocumentParams → Lean.Server.RequestM Unit)
  (lastTaskMutex : Std.Mutex (Lean.Server.ServerTask Unit)) (initState : Dynamic) (stateRef : IO.Ref Dynamic)
  (completeness : Lean.Server.RequestHandlerCompleteness)
  (fileSource_1 : Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri)
  (pureHandle_1 : Lean.Json → Dynamic → Lean.Server.RequestM (Lean.Server.SerializedLspResponse × Dynamic))
  (handle_1 : Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse))
  (pureOnDidChange_1 : Lean.Lsp.DidChangeTextDocumentParams → StateT Dynamic Lean.Server.RequestM Unit)
  (onDidChange_1 : Lean.Lsp.DidChangeTextDocumentParams → Lean.Server.RequestM Unit)
  (lastTaskMutex_1 : Std.Mutex (Lean.Server.ServerTask Unit)) (initState_1 : Dynamic) (stateRef_1 : IO.Ref Dynamic)
  (completeness_1 : Lean.Server.RequestHandlerCompleteness),
  ({ fileSource := fileSource, pureHandle := pureHandle, handle := handle, pureOnDidChange := pureOnDidChange,
        onDidChange := onDidChange, lastTaskMutex := lastTaskMutex, initState := initState, stateRef := stateRef,
        completeness := completeness } =
      { fileSource := fileSource_1, pureHandle := pureHandle_1, handle := handle_1,
        pureOnDidChange := pureOnDidChange_1, onDidChange := onDidChange_1, lastTaskMutex := lastTaskMutex_1,
        initState := initState_1, stateRef := stateRef_1, completeness := completeness_1 }) =
    (fileSource = fileSource_1 ∧
      pureHandle = pureHandle_1 ∧
        handle = handle_1 ∧
          pureOnDidChange = pureOnDidChange_1 ∧
            onDidChange = onDidChange_1 ∧
              lastTaskMutex = lastTaskMutex_1 ∧
                initState = initState_1 ∧ stateRef = stateRef_1 ∧ completeness = completeness_1)
-- Init.Data.SInt.Bitwise
instCommutativeISizeHXor : Std.Commutative fun x1 x2 => x1 ^^^ x2
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- A function which can be uniformly approximated by uniformly continuous functions is uniformly
continuous.  -/
uniformContinuous_of_uniform_approx_of_uniformContinuous : ∀ {α : Type u_4} {β : Type u_5} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  (∀ u ∈ uniformity β, ∃ F, UniformContinuous F ∧ ∀ (y : α), (f y, F y) ∈ u) → UniformContinuous f
-- Lean.Elab.Tactic.Grind.Basic
/-- Cache for `BackwardRule`s created from declaration names (sym mode only).  -/
Lean.Elab.Tactic.Grind.Cache.backwardRuleName : Lean.Elab.Tactic.Grind.Cache → Lean.PHashMap Lean.Name Lean.Meta.Sym.BackwardRule
-- Mathlib.Topology.MetricSpace.ProperSpace
/-- A proper space is locally compact  -/
locallyCompact_of_proper : ∀ {α : Type u} [inst : PseudoMetricSpace α] [ProperSpace α], LocallyCompactSpace α
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.map_le_localized₀ : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N)
  [inst_5 : IsLocalizedModule p f] (M' : Submodule R M), Submodule.map f M' ≤ Submodule.localized₀ p f M'
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.instInhabitedState.default : Lean.Meta.Grind.AC.State
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.isIso_truncGT_map_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {Y Z : C} (g : Y ⟶ Z) (n : ℤ),
  CategoryTheory.IsIso ((t.truncGT n).map g) ↔
    ∃ X f h,
      ∃ (_ :
        CategoryTheory.Pretriangulated.Triangle.mk f (CategoryTheory.CategoryStruct.comp g ((t.truncGTπ n).app Z)) h ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles),
        t.IsLE X n
-- Init.Data.List.Lemmas
List.or_all_distrib_right : ∀ {α : Type u_1} {l : List α} {p : α → Bool} {q : Bool}, (l.all p || q) = l.all fun a => p a || q
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
/-- Given two composable morphisms `f` and `g` in the category of cochain complexes, this
is the canonical morphism (which is a homotopy equivalence) from `mappingCone g` to
the mapping cone of the morphism `mappingCone f ⟶ mappingCone (f ≫ g)`.  -/
CochainComplex.MappingConeCompHomotopyEquiv.hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {X₁ X₂ X₃ : CochainComplex C ℤ} →
          (f : X₁ ⟶ X₂) →
            (g : X₂ ⟶ X₃) →
              CochainComplex.mappingCone g ⟶
                CochainComplex.mappingCone (CochainComplex.mappingConeCompTriangle f g).mor₁
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.add_left : ∀ {α : Type u} {β : Type v} {l : Filter α} [inst : Add β] {f₁ f₂ f₃ : α → β}, f₁ =ᶠ[l] f₂ → f₃ + f₁ =ᶠ[l] f₃ + f₂
-- Mathlib.Analysis.MeanInequalities
/-- **AM-GM inequality - strict inequality condition**: This theorem provides the strict inequality
condition for the *positive* weighted version of the AM-GM inequality for real-valued nonnegative
functions.

The condition is that not all elements of `z` are equal to each other;
see `geom_mean_lt_arith_mean_weighted_iff_of_pos'` for a version that compares the elements to their
center of mass `∑ i ∈ s, w i * z i` instead.  -/
Real.geom_mean_lt_arith_mean_weighted_iff_of_pos : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 < w i) →
    ∑ i ∈ s, w i = 1 → (∀ i ∈ s, 0 ≤ z i) → (∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i ↔ ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k)
-- Init.Data.Int.Order
Int.toNat_zero : Int.toNat 0 = 0
-- Lean.Parser.Term
Lean.Parser.Term.dotIdent.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- The equivalence between `gammaSet 1 r 0` and `gammaSet 1 1 0` for non-zero `r`.  -/
EisensteinSeries.gammaSetDivGcdEquiv : (r : ℕ) → [NeZero r] → ↑(EisensteinSeries.gammaSet 1 r 0) ≃ ↑(EisensteinSeries.gammaSet 1 1 0)
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.IsFormalAdjoint.symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F}
  {S : F →ₗ.[𝕜] E}, T.IsFormalAdjoint S → S.IsFormalAdjoint T
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.isInitialIso_apply : ∀ (x : { x // x.IsInitial }), Ordinal.isInitialIso x = (↑x).card
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_tensorObj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : Cᵒᵖ),
  Opposite.unop (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (Opposite.unop X) (Opposite.unop Y)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denoteAsIntModule.go.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (acc : α),
  Lean.Grind.CommRing.Mon.denoteAsIntModule.go ctx Lean.Grind.CommRing.Mon.unit acc = acc
-- Lean.Elab.Tactic.Location
/-- Denotes a set of locations where a tactic should be applied for the main goal. See also `withLocation`.  -/
Lean.Elab.Tactic.Location : Type
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.le_of_add_le_add_left : ∀ {d : ℕ} [dnsq : Zsqrtd.Nonsquare d] (a b c : ℤ√↑d), c + a ≤ c + b → a ≤ b
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.not_dep_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, autoParam (X ⊆ M.E) Matroid.not_dep_iff._auto_1 → (¬M.Dep X ↔ M.Indep X)
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- Typeclass expressing that for all `G`-split pairs `f,g`, `G` preserves colimits of
`parallelPair f g`.  -/
CategoryTheory.Monad.PreservesColimitOfIsSplitPair : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] → CategoryTheory.Functor D C → Prop
-- Init.Data.Rat.Lemmas
Rat.mk_den_one : ∀ {r : ℤ}, { num := r, den_nz := Nat.one_ne_zero, reduced := ⋯ } = ↑r
-- Init.Data.UInt.Bitwise
UInt16.toBitVec_xor : ∀ (a b : UInt16), (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryGT?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getEntryGT? k = t₂.getEntryGT? k