mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.brecOn.go : {motive : Lean.Grind.CommRing.Mon → Sort u} →
  (t : Lean.Grind.CommRing.Mon) →
    ((t : Lean.Grind.CommRing.Mon) → Lean.Grind.CommRing.Mon.below t → motive t) →
      motive t ×' Lean.Grind.CommRing.Mon.below t
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited γ] {f : α → β → γ} {k k' : α},
  t.getKey? k = some k' → (Std.ExtTreeMap.map f t)[k]! = (Option.map (f k') t[k]?).get!
-- Init.Data.UInt.Lemmas
USize.mod_one : ∀ {a : USize}, a % 1 = 0
-- Mathlib.Algebra.Ring.Subring.Defs
SubringClass.addSubgroupClass : ∀ (S : Type u_1) (R : Type u) [inst : SetLike S R] [inst_1 : NonAssocRing R] [h : SubringClass S R],
  AddSubgroupClass S R
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.fromOpcycles_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i j : ι} [inst_2 : K.HasHomology i],
  ¬c.Rel i j → K.fromOpcycles i j = 0
-- Std.Time.Format
/-- Formats a `DateTime` value into an ISO8601 string.
 -/
Std.Time.DateTime.toISO8601String : Std.Time.DateTime → String
-- Mathlib.CategoryTheory.Limits.Creates
/-- a cocone in the source category of the functor  -/
CategoryTheory.LiftableCocone.liftedCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                {c : CategoryTheory.Limits.Cocone (K.comp F)} →
                  CategoryTheory.LiftableCocone K F c → CategoryTheory.Limits.Cocone K
-- Lean.Elab.Command
_private.Lean.Elab.Command.0.Lean.Elab.Command.recordUsedSyntaxKinds : Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Algebra.Order.Ring.Archimedean
OrderMonoidHomClass.toOrderAddMonoidHom.congr_simp : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] [inst_4 : FunLike F α β] [inst_5 : OrderHomClass F α β] [inst_6 : AddMonoidHomClass F α β]
  (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Mathlib.MeasureTheory.Measure.Stieltjes
Iotop.eq_1 : ∀ {R : Type u_1} [inst : LinearOrder R] (a b : R), Iotop a b = if IsTop b then Set.Ioc a b else Set.Ioo a b
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isSome_getElem?_toArray_roc_eq : ∀ {m n i : ℕ}, ((m<...=n).toArray[i]?.isSome = true) = (i < n - m)
-- Mathlib.Algebra.Group.Prod
AddUnits.embedProduct.eq_1 : ∀ (α : Type u_6) [inst : AddMonoid α],
  AddUnits.embedProduct α = { toFun := fun x => (↑x, AddOpposite.op ↑(-x)), map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Data.PFunctor.Multivariate.Basic
/-- Applying `P` to an object of `Type`  -/
MvPFunctor.Obj : {n : ℕ} → MvPFunctor.{u} n → TypeVec.{u} n → Type u
-- Mathlib.Topology.ContinuousMap.Basic
/-- The continuous functions from `α` to `β` are the same as the plain functions when `α` is discrete.
 -/
ContinuousMap.equivFnOfDiscrete : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → [DiscreteTopology α] → C(α, β) ≃ (α → β)
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.getFVarIds : Array Lean.Syntax → Lean.Elab.Tactic.TacticM (Array Lean.FVarId)
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curry0_uncurry0 : ∀ (𝕜 : Type u) (G : Type wG) {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (x : G'),
  (ContinuousMultilinearMap.uncurry0 𝕜 G x).curry0 = x
-- Aesop.Script.SpecificTactics
Aesop.replaceFVarS : Lean.MVarId → Lean.FVarId → Lean.Expr → Lean.Expr → Aesop.ScriptM (Lean.MVarId × Lean.FVarId × Bool)
-- Lean.Elab.Term.TermElabM
/-- Postpone the elaboration of `stx`, return a metavariable that acts as a placeholder, and
ensures the info tree is updated and a hole id is introduced.
When `stx` is elaborated, new info nodes are created and attached to the new hole id in the info tree.
 -/
Lean.Elab.Term.postponeElabTerm : Lean.Syntax → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mulC_nc : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (p₁.mulC_nc p₂ c) =
    Lean.Grind.CommRing.Poly.denote ctx p₁ * Lean.Grind.CommRing.Poly.denote ctx p₂
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
left_eq_midpoint_iff : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y : P}, x = midpoint R x y ↔ x = y
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_iSup_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {ι : Type u_5} {f : M →ₙ+ N},
  Function.Injective ⇑f →
    ∀ (S : ι → AddSubsemigroup M), AddSubsemigroup.comap f (⨆ i, AddSubsemigroup.map f (S i)) = iSup S
-- Mathlib.Combinatorics.Hindman
Hindman.FP.head' : ∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M), Hindman.FP a a.head
-- Mathlib.Data.Num.ZNum
ZNum.bit0.eq_3 : ∀ (a : PosNum), (ZNum.neg a).bit0 = ZNum.neg a.bit0
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.mapNatTrans_τ₂ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  {F G : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms]
  (τ : F ⟶ G), (S.mapNatTrans τ).τ₂ = τ.app S.X₂
-- Init.System.IOError
IO.Error.mkPermissionDenied : UInt32 → String → IO.Error
-- Batteries.Data.String.Lemmas
String.takeWhile_eq : ∀ (p : Char → Bool) (s : String), String.Legacy.takeWhile s p = String.ofList (List.takeWhile p s.toList)
-- Mathlib.Data.Multiset.Fintype
/-- The embedding from a multiset into `α × ℕ` where the second coordinate enumerates repeats.
If you are looking for the function `m → α`, that would be plain `(↑)`.  -/
Multiset.coeEmbedding : {α : Type u_1} → [inst : DecidableEq α] → (m : Multiset α) → m.ToType ↪ α × ℕ
-- Mathlib.RingTheory.ClassGroup.Basic
FractionalIdeal.unitsMulEquivSubmodule.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P],
  FractionalIdeal.unitsMulEquivSubmodule =
    { toFun := (↑(Units.map ↑(FractionalIdeal.coeSubmoduleHom S P))).toFun,
      invFun := fun I => { val := ⟨↑I, ⋯⟩, inv := ⟨↑I⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }, left_inv := ⋯,
      right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inr_inl_pushoutLeftPushoutInrIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'] {Z_1 : C}
  (h : CategoryTheory.Limits.pushout f (CategoryTheory.CategoryStruct.comp g g') ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushout.inr f g) g')
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom h)) =
    CategoryTheory.CategoryStruct.comp g'
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.inr f (CategoryTheory.CategoryStruct.comp g g')) h)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccLimit_mul_left : ∀ {a b : Ordinal.{u_4}}, Order.IsSuccLimit a → 0 < b → Order.IsSuccLimit (a * b)
-- Std.Data.String.ToInt
String.isInt_iff : ∀ {s : String}, s.isInt = true ↔ s.isNat = true ∨ ∃ t, s = "-" ++ t ∧ t.isNat = true
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.projectiveDimension_ge_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C) (n : ℕ),
  ↑n ≤ CategoryTheory.projectiveDimension X ↔ ¬CategoryTheory.HasProjectiveDimensionLT X n
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.instAddMonoid : {α : Type u} → [inst : AddMonoid α] → AddMonoid (AddUnits α)
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Submodule.topologicalClosure_eq_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥K], K.topologicalClosure = K
-- Mathlib.Topology.Semicontinuity.Basic
IsOpen.upperSemicontinuousWithinAt_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s t : Set α} {x : α} {y : β} [inst_1 : Zero β]
  [inst_2 : Preorder β], IsOpen s → y ≤ 0 → UpperSemicontinuousWithinAt (s.indicator fun _x => y) t x
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.instInhabited : (basis_hd : ℝ → ℝ) →
  (basis_tl : Tactic.ComputeAsymptotics.Basis) →
    Inhabited (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl)
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instDecidableMem : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] →
        [inst_2 : EquivBEq α] → [inst_3 : LawfulHashable α] → {m : Std.ExtHashMap α β} → {a : α} → Decidable (a ∈ m)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.foldlM.match_1.eq_1 : ∀ {σ : Type u_3} {α : Type u_1} (motive : σ → RBTree.RBNode α → Sort u_2) (b : σ)
  (h_1 : (b : σ) → motive b RBTree.RBNode.nil)
  (h_2 :
    (b : σ) →
      (c : RBTree.RBColor) →
        (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive b (RBTree.RBNode.node c l v r)),
  (match b, RBTree.RBNode.nil with
    | b, RBTree.RBNode.nil => h_1 b
    | b, RBTree.RBNode.node c l v r => h_2 b c l v r) =
    h_1 b
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.commRingNorm : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr →
  Lean.Meta.Grind.Arith.CommRing.RingExpr → Lean.Grind.CommRing.Poly → Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof
-- Mathlib.AlgebraicTopology.CechNerve
/-- A helper function used in defining the Čech conerve adjunction.  -/
CategoryTheory.CosimplicialObject.cechConerveEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 :
        ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
          CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] →
      (F : CategoryTheory.Arrow C) →
        (X : CategoryTheory.CosimplicialObject.Augmented C) →
          (F.augmentedCechConerve ⟶ X) ≃ (F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X)
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.isColimitLocallyConstantPresheaf_desc_apply : ∀ {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite))
  (X : Type u) (hc : CategoryTheory.Limits.IsLimit c) [inst : ∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)]
  (s :
    CategoryTheory.Limits.Cocone
      ((F.comp FintypeCat.toLightProfinite).op.comp (LightCondensed.locallyConstantPresheaf X)))
  (n : ℕᵒᵖ) (f : LocallyConstant (↑(FintypeCat.toLightProfinite.obj (F.obj n)).toTop) X),
  (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isColimitLocallyConstantPresheaf c X hc).desc s))
      (LocallyConstant.comap (TopCat.Hom.hom (c.π.app n).hom) f) =
    (CategoryTheory.ConcreteCategory.hom (s.ι.app (Opposite.op n))) f
-- Mathlib.Data.Nat.GCD.BigOperators
Nat.coprime_prod_left_iff : ∀ {ι : Type u_1} {t : Finset ι} {s : ι → ℕ} {x : ℕ}, (∏ i ∈ t, s i).Coprime x ↔ ∀ i ∈ t, (s i).Coprime x
-- Mathlib.Probability.Process.Stopping
MeasureTheory.integrable_stoppedProcess : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {μ : MeasureTheory.Measure Ω}
  {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E} [inst_1 : LinearOrder ι] [inst_2 : TopologicalSpace ι]
  [OrderTopology ι] [FirstCountableTopology ι] {ℱ : MeasureTheory.Filtration ι m} [inst_5 : NormedAddCommGroup E]
  [LocallyFiniteOrderBot ι],
  MeasureTheory.IsStoppingTime ℱ τ →
    (∀ (n : ι), MeasureTheory.Integrable (u n) μ) →
      ∀ (n : ι), MeasureTheory.Integrable (MeasureTheory.stoppedProcess u τ n) μ
-- Mathlib.RingTheory.Localization.BaseChange
Submonoid.map_isUnit_le_isUnit : ∀ {M : Type u_7} {N : Type u_8} [inst : Monoid M] [inst_1 : Monoid N] {F : Type u_9} [inst_2 : FunLike F M N]
  [inst_3 : MonoidHomClass F M N] (f : F), Submonoid.map f (IsUnit.submonoid M) ≤ IsUnit.submonoid N
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.lift_comp_ι : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (g : FreeAlgebra R X →ₐ[R] A), (FreeAlgebra.lift R) (⇑g ∘ FreeAlgebra.ι R) = g
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.val_inv_toUnits_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : ↥(spinGroup Q)), ↑(spinGroup.toUnits x)⁻¹ = ↑x⁻¹
-- Mathlib.ModelTheory.Bundled
/-- The underlying type for the models  -/
FirstOrder.Language.Theory.ModelType.Carrier : {L : FirstOrder.Language} → {T : L.Theory} → T.ModelType → Type w
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.processValue : Lean.Meta.Match.Problem → Lean.MetaM (Array Lean.Meta.Match.Problem)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
ContDiffWithinAt.rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : E → ℝ} {x : E} {s : Set E}
  {n : WithTop ℕ∞},
  ContDiffWithinAt ℝ n f s x → ContDiffWithinAt ℝ n g s x → f x ≠ 0 → ContDiffWithinAt ℝ n (fun x => f x ^ g x) s x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.compare_maxKey?_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β} {km kmm : α} (hkm : t.maxKey? = some km),
  (Std.DTreeMap.Const.modify t k f).maxKey?.get ⋯ = kmm → cmp kmm km = Ordering.eq
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.isRatStieltjesPoint_defaultRatCDF : ∀ {α : Type u_1} (a : α), ProbabilityTheory.IsRatStieltjesPoint (fun x => ProbabilityTheory.defaultRatCDF) a
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.generalLinearGroup_is_two_pretransitive : ∀ (K : Type u_2) (V : Type u_3) [inst : AddCommGroup V] [inst_1 : DivisionRing K] [inst_2 : Module K V],
  MulAction.IsMultiplyPretransitive (LinearMap.GeneralLinearGroup K V) (Projectivization K V) 2
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.instElemOrbit_1 : {G : Type u_1} →
  {α : Type u_2} →
    [inst : Group G] → [inst_1 : MulAction G α] → (x : MulAction.orbitRel.Quotient G α) → MulAction G ↑x.orbit
-- Mathlib.Computability.Language
/-- **Arden's lemma**  -/
Language.self_eq_mul_add_iff : ∀ {α : Type u_1} {l m n : Language α}, [] ∉ m → (l = m * l + n ↔ l = KStar.kstar m * n)
-- Mathlib.Topology.Category.CompHaus.EffectiveEpi
CompHaus.instPreregular : CategoryTheory.Preregular CompHaus
-- Mathlib.CategoryTheory.Subobject.WellPowered
CategoryTheory.WellPowered.subobject_small : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v, u₁} C} {inst_1 : CategoryTheory.LocallySmall.{w, v, u₁} C}
  [self : CategoryTheory.WellPowered.{w, v, u₁} C] (X : C), Small.{w, max u₁ v} (CategoryTheory.Subobject X)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_trans_of_half_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b c : E} {t : ℝ}
  (ω : E → E →L[𝕜] F) (γab : Path a b) (γbc : Path b c),
  1 / 2 < t → curveIntegralFun ω (γab.trans γbc) t = 2 • curveIntegralFun ω γbc (2 * t - 1)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonDidCloseTextDocumentParams.fromJson : Lean.Json → Except String Lean.Lsp.DidCloseTextDocumentParams
-- Mathlib.Algebra.Group.Prod
Prod.mk_zero_add_mk_zero : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : AddZeroClass N] (a₁ a₂ : M), (a₁, 0) + (a₂, 0) = (a₁ + a₂, 0)
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.TopSort.State : Type
-- Mathlib.Logic.Equiv.Basic
Function.Involutive.toPerm_symm : ∀ {α : Sort u_1} {f : α → α} (h : Function.Involutive f),
  Equiv.symm (Function.Involutive.toPerm f h) = Function.Involutive.toPerm f h
-- Mathlib.MeasureTheory.Integral.CircleAverage
Real.circleAverage.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℂ → E) (c : ℂ) (R : ℝ),
  Real.circleAverage f c R = (2 * Real.pi)⁻¹ • ∫ (θ : ℝ) in 0..2 * Real.pi, f (circleMap c R θ)
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.preprocess : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Complex.deriv_tan : ∀ (x : ℂ), deriv Complex.tan x = 1 / Complex.cos x ^ 2
-- Init.Data.Vector.Lemmas
Vector.firstM_mk : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Alternative m] {f : α → m β} {xs : Array α}
  (h : xs.size = n), Vector.firstM f (Vector.mk xs h) = Array.firstM f xs
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.mul_eq_mul_of_eq : ∀ {A : Type u_2} [sA : CommSemiring A] {c a b : A}, a = b → c * a = c * b
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.instLawfulMonadLiftOfLawfulMonadLiftFunction : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] {lift : ⦃α : Type u⦄ → m α → n α}
  [Std.Internal.LawfulMonadLiftFunction lift], LawfulMonadLift m n
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.id.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.AddMon C), M.id = { hom := CategoryTheory.CategoryStruct.id M.X, isAddMonHom_hom := ⋯ }
-- Mathlib.Order.Interval.Set.Defs
Set.Iic.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (b : α), Set.Iic b = {x | x ≤ b}
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeries.eq_ge_of_eq_succ : ∀ {G : Type u_1} [inst : AddGroup G] {a b : ℕ},
  a ≤ b →
    AddSubgroup.upperCentralSeries G a = AddSubgroup.upperCentralSeries G (a + 1) →
      AddSubgroup.upperCentralSeries G a = AddSubgroup.upperCentralSeries G b
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α],
  MulOpposite.instCommMonoid = { toMonoid := MulOpposite.instMonoid, mul_comm := ⋯ }
-- Init.Data.Int.Order
Int.neg_le_sub_right_of_le_add : ∀ {a b c : ℤ}, c ≤ a + b → -b ≤ a - c
-- Lean.Meta.Match.CaseValues
_private.Lean.Meta.Match.CaseValues.0.Lean.Meta.caseValues.loop : Lean.FVarId →
  Lean.Name →
    Bool →
      ℕ →
        Lean.MVarId →
          List Lean.Expr →
            Array Lean.FVarId → Array Lean.Meta.CaseValuesSubgoal → Lean.MetaM (Array Lean.Meta.CaseValuesSubgoal)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max_eq_get_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {he : t.isEmpty = false},
  t.max he = t.max?.get ⋯
-- Mathlib.Topology.ShrinkingLemma
/-- For each `i ∈ carrier`, the original set includes the closure of the refined set.  -/
ShrinkingLemma.PartialRefinement.closure_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  (self : ShrinkingLemma.PartialRefinement u s p) {i : ι}, i ∈ self.carrier → closure (self.toFun i) ⊆ u i
-- Mathlib.Algebra.Group.Hom.Defs
/-- The proposition that the function preserves 0  -/
ZeroHomClass.map_zero : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} {inst : Zero M} {inst_1 : Zero N}
  {inst_2 : FunLike F M N} [self : ZeroHomClass F M N] (f : F), f 0 = 0
-- Mathlib.RingTheory.AdicCompletion.Exactness
/-- Inductively construct preimage of Cauchy sequence in kernel of `g.adicCompletion I`.  -/
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapExactAux : {R : Type u} →
  [inst : CommRing R] →
    {I : Ideal R} →
      {M : Type u} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {N : Type u} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {P : Type u} →
                    [inst_5 : AddCommGroup P] →
                      [inst_6 : Module R P] →
                        {f : M →ₗ[R] N} →
                          {g : N →ₗ[R] P} →
                            Function.Injective ⇑f →
                              Function.Exact ⇑f ⇑g →
                                Function.Surjective ⇑g →
                                  {k : ℕ} →
                                    (∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)) →
                                      (x : AdicCompletion.AdicCauchySequence I N) →
                                        (∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤) →
                                          (n : ℕ) → ↑{a | f a - ↑x (k + n) ∈ I ^ (k + n) • ⊤}
-- Mathlib.Probability.Distributions.Pareto
ProbabilityTheory.paretoPDF_eq : ∀ (t r x : ℝ), ProbabilityTheory.paretoPDF t r x = ENNReal.ofReal (if t ≤ x then r * t ^ r * x ^ (-(r + 1)) else 0)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
addRightMono_of_addLeftMono : ∀ (N : Type u_2) [inst : AddCommSemigroup N] [inst_1 : LE N] [AddLeftMono N], AddRightMono N
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_hom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (Y : CategoryTheory.Over X),
  CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom =
    CategoryTheory.ChosenPullbacksAlong.fst Y.hom (CategoryTheory.CategoryStruct.id X)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_eq_getD_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α} {fallback : β}, Std.ExtDTreeMap.Const.getD t a fallback = (Std.ExtDTreeMap.Const.get? t a).getD fallback
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousWithinAt.nnnorm : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {s : Set α}
  {a : α}, ContinuousWithinAt f s a → ContinuousWithinAt (fun x => ‖f x‖₊) s a
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.InvariantForm.apply_root_ne_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (B : P.InvariantForm)
  (i : ι), B.form (P.root i) ≠ 0
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_zero' : ∀ {w₁ w₂ : ℕ} {x : BitVec w₁}, x <<< 0#w₂ = x
-- Init.Data.Rat.Lemmas
Rat.inv_zero : 0⁻¹ = 0
-- Mathlib.Algebra.BigOperators.Finprod
finprod_eq_prod_plift_of_mulSupport_subset : ∀ {M : Type u_2} {α : Sort u_4} [inst : CommMonoid M] {f : α → M} {s : Finset (PLift α)},
  Function.mulSupport (f ∘ PLift.down) ⊆ ↑s → ∏ᶠ (i : α), f i = ∏ i ∈ s, f i.down
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Associated.pow_iff : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsIntegrallyClosed R] {n : ℕ},
  n ≠ 0 → ∀ {a b : R}, Associated (a ^ n) (b ^ n) ↔ Associated a b