mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Compiler.LCNF.Basic
/-- Projecting non-USize scalars out of a value
 -/
Lean.Compiler.LCNF.LetValue.sproj : {pu : Lean.Compiler.LCNF.Purity} →
  ℕ →
    ℕ →
      Lean.FVarId →
        autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_11 →
          Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Algebra.Lie.Solvable
Function.Surjective.lieAlgebra_isSolvable : ∀ {R : Type u} {L : Type v} {L' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] {f : L' →ₗ⁅R⁆ L} [hL' : LieAlgebra.IsSolvable L'],
  Function.Surjective ⇑f → LieAlgebra.IsSolvable L
-- Mathlib.Data.List.Palindrome
List.Palindrome.of_reverse_eq : ∀ {α : Type u_1} {l : List α}, l.reverse = l → l.Palindrome
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The codomain of a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.WhiskerRight.tgtM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.WhiskerRight → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Init.Data.Int.Order
Int.zero_eq_toNat_sub_iff : ∀ (m n : ℤ), 0 = (m - n).toNat ↔ m ≤ n
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.SplitKind.considerMatch : Lean.Meta.SplitKind → Bool
-- Mathlib.Order.Heyting.Hom
/-- The type of Heyting homomorphisms from `α` to `β`. Bounded lattice homomorphisms that preserve
Heyting implication.  -/
HeytingHom : (α : Type u_6) → (β : Type u_7) → [HeytingAlgebra α] → [HeytingAlgebra β] → Type (max u_6 u_7)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.revAll_bool_eq : ∀ {p : Char → Bool} {s : String}, s.revAll p = s.toList.all p
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.continuous_apply : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → TopologicalSpace (β i)] (i : ι),
  Continuous fun f => f.ofLp i
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.f'_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData), CategoryTheory.CategoryStruct.comp h.f' h.π = 0
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.power_ne_zero : ∀ {a : Cardinal.{u_1}} (b : Cardinal.{u_1}), a ≠ 0 → a ^ b ≠ 0
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.forgetToQuiv_obj : ∀ (V : CategoryTheory.ReflQuiv), CategoryTheory.ReflQuiv.forgetToQuiv.obj V = CategoryTheory.Quiv.of ↑V
-- Mathlib.Data.List.Basic
List.map_involutive_iff : ∀ {α : Type u} {f : α → α}, Function.Involutive (List.map f) ↔ Function.Involutive f
-- Init.Data.UInt.Bitwise
UInt8.toFin_shiftRight : ∀ (a b : UInt8), b < 8 → (a >>> b).toFin = a.toFin >>> b.toFin
-- Init.Data.String.Bootstrap
String.Internal.get : String → String.Pos.Raw → Char
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableAt.of_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {E' : Type u_4}
  [inst_5 : AddCommGroup E'] [inst_6 : Module 𝕜 E'] {f : E → F} {x : E'} {L : E' →ₗ[𝕜] E} {v : E'},
  LineDifferentiableAt 𝕜 (f ∘ ⇑L) x v → LineDifferentiableAt 𝕜 f (L x) (L v)
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.instCreatesColimitWalkingParallelPairParallelPairOfIsSplitPairOfCreatesColimitOfIsSplitPair : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {A B : D} →
            (f g : A ⟶ B) →
              [G.IsSplitPair f g] →
                [CategoryTheory.Monad.CreatesColimitOfIsSplitPair G] →
                  CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair f g) G
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.PartialMap.comp_domain : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f : X.PartialMap Y)
  [inst_2 : AlgebraicGeometry.IsDominant f.hom] (g : Y.PartialMap Z),
  (f.comp g).domain =
    (AlgebraicGeometry.Scheme.Hom.opensFunctor f.domain.ι).obj ((TopologicalSpace.Opens.map f.hom.base).obj g.domain)
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- Fixed points of sup of submonoids is intersection  -/
fixedPoints_submonoid_sup : ∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : MulAction M α] {P Q : Submonoid M},
  MulAction.fixedPoints (↥(P ⊔ Q)) α = MulAction.fixedPoints (↥P) α ∩ MulAction.fixedPoints (↥Q) α
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {b : R}, b * p.leadingCoeff = 1 → (Polynomial.C b * p).Monic
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- **Alias** of `Affine.Simplex.closedInterior_sdiff_interior`. -/
Affine.Simplex.closedInterior_diff_interior : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : LinearOrder k] [IsOrderedAddMonoid k] [ZeroLEOneClass k] {n : ℕ}
  [inst_7 : NeZero n] (s : Affine.Simplex k P n), s.closedInterior \ s.interior = ⋃ i, (s.faceOpposite i).closedInterior
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.All.del : ∀ {α : Type u_1} {p : α → Prop} {cut : α → Ordering} {t : RBTree.RBNode α},
  RBTree.RBNode.All p t → RBTree.RBNode.All p (RBTree.RBNode.del cut t)
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f)
  (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)}
  (h : (F.map f₂₃).toFunctor.obj ((F.map f₁₂).toFunctor.obj ((F.map f₀₁).toFunctor.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp
        ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X)) h) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp
        ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) h)
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_sieve_of_pullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)},
  E.IsStronglySheafFor F →
    (∀ ⦃Y : C⦄ (f : Y ⟶ X),
        CategoryTheory.Presieve.IsSeparatedFor F (CategoryTheory.Sieve.pullback f E.sieve₀).arrows) →
      ∀ {S : CategoryTheory.Sieve X},
        (∀ (i : E.I₀), CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Sieve.pullback (E.f i) S).arrows) →
          (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
              CategoryTheory.Presieve.IsSeparatedFor F
                (CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) S).arrows) →
            CategoryTheory.Presieve.IsSheafFor F S.arrows
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.const_mul_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal)
  (x : ENNReal), (MeasureTheory.SimpleFunc.const α x * f).lintegral μ = x * f.lintegral μ
-- Mathlib.Algebra.Algebra.RestrictScalars
/-- The `R`-algebra homomorphism from the original coefficient algebra `S` to endomorphisms
of `RestrictScalars R S M`.
 -/
RestrictScalars.lsmul : (R : Type u_1) →
  (S : Type u_2) →
    (M : Type u_3) →
      [inst : Semiring S] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : CommSemiring R] →
            [inst_3 : Algebra R S] → [inst_4 : Module S M] → S →ₐ[R] Module.End R (RestrictScalars R S M)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.mul_toFun : ∀ {t1 t2 : Tactic.ComputeAsymptotics.Monomial} {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    List.length t1.unit = List.length t2.unit → (t1.mul t2).toFun basis =ᶠ[Filter.atTop] t1.toFun basis * t2.toFun basis
-- Mathlib.LinearAlgebra.Charpoly.Basic
/-- Any endomorphism power can be computed as the sum of endomorphism powers less than the
dimension of the module.  -/
LinearMap.pow_eq_aeval_mod_charpoly : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M) (k : ℕ),
  f ^ k = (Polynomial.aeval f) (Polynomial.X ^ k %ₘ f.charpoly)
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- Taking the product of two maps with the same domain is equivalent to taking the product of
their codomains.  -/
NonUnitalAlgHom.prodEquiv : {R : Type u} →
  [inst : Monoid R] →
    {A : Type v} →
      {B : Type w} →
        {C : Type w₁} →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : DistribMulAction R A] →
              [inst_3 : NonUnitalNonAssocSemiring B] →
                [inst_4 : NonUnitalNonAssocSemiring C] →
                  [inst_5 : DistribMulAction R B] →
                    [inst_6 : DistribMulAction R C] → (A →ₙₐ[R] B) × (A →ₙₐ[R] C) ≃ (A →ₙₐ[R] B × C)
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.getLhs : Lean.Elab.Tactic.TacticM Lean.Expr
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.mk.sizeOf_spec : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : SizeOf α] (val neg : α) (val_neg : val + neg = 0)
  (neg_val : neg + val = 0),
  sizeOf { val := val, neg := neg, val_neg := val_neg, neg_val := neg_val } =
    1 + sizeOf val + sizeOf neg + sizeOf val_neg + sizeOf neg_val
-- Mathlib.Data.Finsupp.Defs
Finsupp.instSubsingleton' : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] [Subsingleton M], Subsingleton (α →₀ M)
-- Init.Data.Array.Lemmas
Array.getElem_eq_getElem_reverse : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size), xs[i] = xs.reverse[xs.size - 1 - i]
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.top_N : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R},
  ⊤.N = ⊤
-- Lean.Util.SCC
Lean.SCC.State.mk.sizeOf_spec : ∀ {α : Type} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] (stack : List α) (nextIndex : ℕ)
  (data : Std.HashMap α Lean.SCC.Data) (sccs : List (List α)),
  sizeOf { stack := stack, nextIndex := nextIndex, data := data, sccs := sccs } =
    1 + sizeOf stack + sizeOf nextIndex + sizeOf data + sizeOf sccs
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : SizeOf C] {X₁ X₂ X₃ : C} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  (zero : autoParam (CategoryTheory.CategoryStruct.comp f g = 0) CategoryTheory.ShortComplex.zero._autoParam),
  sizeOf { X₁ := X₁, X₂ := X₂, X₃ := X₃, f := f, g := g, zero := zero } =
    1 + sizeOf X₁ + sizeOf X₂ + sizeOf X₃ + sizeOf f + sizeOf g + sizeOf zero
-- Init.Data.Ord.Basic
_private.Init.Data.Ord.Basic.0.Ordering.swap.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_1 ()
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- The counit is natural in both `S : CompHausLike P` and
`Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))`  -/
CompHausLike.LocallyConstant.counit : (P : TopCat → Prop) →
  [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] →
    [inst : CompHausLike.HasProp P PUnit.{u + 1}] →
      [inst_1 : CompHausLike.HasExplicitFiniteCoproducts P] →
        [inst_2 : CompHausLike.HasExplicitPullbacks P] →
          (hs :
              ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
                CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) →
            [CompHausLike.HasExplicitFiniteCoproducts P] →
              ((CategoryTheory.sheafSections (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))).obj
                      (Opposite.op (CompHausLike.of P PUnit.{u + 1}))).comp
                  (CompHausLike.LocallyConstant.functor P hs) ⟶
                CategoryTheory.Functor.id
                  (CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w)))
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.instMulRingNormClassOfNontrivialOfIsDomain : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing S] [inst_1 : PartialOrder S] [IsOrderedRing S] [inst_3 : Ring R]
  [NoZeroDivisors S] [Nontrivial R] [IsDomain S], MulRingNormClass (AbsoluteValue R S) R S
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.denote : Nat.Internal.Linear.Context → Nat.Internal.SOM.Expr → ℕ
-- Mathlib.Analysis.Normed.Group.Basic
/-- A scaled sphere is a sphere.  -/
setOf_div_mem_sphere_eq_sphere'' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a : E} {r : ℝ}, {x | x / a ∈ Metric.sphere 1 r} = Metric.sphere a r
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetsExtEntry.local.sizeOf_spec : ∀ (wi : Lean.Widget.WidgetInstance), sizeOf (Lean.Widget.PanelWidgetsExtEntry.local wi) = 1 + sizeOf wi
-- Lean.Meta.Eqns
Lean.Meta.mkEqLikeNameFor : Lean.Environment → Lean.Name → String → Lean.Name
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} {h : (t.get? a).isSome = true}, (t.get? a).get h = t.get a ⋯
-- Mathlib.Data.PFunctor.Multivariate.M
/-- Corecursor for M-type of `P`  -/
MvPFunctor.M.corec' : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u} n} →
      {β : Type v} →
        (g₀ : β → P.A) → ((b : β) → (P.drop.B (g₀ b)).Arrow α) → ((b : β) → P.last.B (g₀ b) → β) → β → P.M α
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.instBEqPoly.beq.match_1.splitter : (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) →
  (x x_1 : Int.Internal.Linear.Poly) →
    ((a b : ℤ) → motive (Int.Internal.Linear.Poly.num a) (Int.Internal.Linear.Poly.num b)) →
      ((a : ℤ) →
          (a_1 : Int.Internal.Linear.Var) →
            (a_2 : Int.Internal.Linear.Poly) →
              (b : ℤ) →
                (b_1 : Int.Internal.Linear.Var) →
                  (b_2 : Int.Internal.Linear.Poly) →
                    motive (Int.Internal.Linear.Poly.add a a_1 a_2) (Int.Internal.Linear.Poly.add b b_1 b_2)) →
        ((x x_2 : Int.Internal.Linear.Poly) →
            (∀ (a b : ℤ), x = Int.Internal.Linear.Poly.num a → x_2 = Int.Internal.Linear.Poly.num b → False) →
              (∀ (a : ℤ) (a_1 : Int.Internal.Linear.Var) (a_2 : Int.Internal.Linear.Poly) (b : ℤ)
                  (b_1 : Int.Internal.Linear.Var) (b_2 : Int.Internal.Linear.Poly),
                  x = Int.Internal.Linear.Poly.add a a_1 a_2 → x_2 = Int.Internal.Linear.Poly.add b b_1 b_2 → False) →
                motive x x_2) →
          motive x x_1
-- Lean.Server.References
/-- Document versions and module references for every module name. Loaded from the current state
in a file worker.
 -/
Lean.Server.WorkerRefMap : Type
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- If `C` is a circuit of `M ／ K`, then `M` has a circuit in the interval `[C, C ∪ K]`.  -/
Matroid.IsCircuit.exists_subset_isCircuit_of_contract : ∀ {α : Type u_1} {M : Matroid α} {K C : Set α}, (M.contract K).IsCircuit C → ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.closure_image : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {s : Set M}
  (f : L.Hom M N),
  (FirstOrder.Language.Substructure.closure L).toFun (⇑f '' s) =
    FirstOrder.Language.Substructure.map f ((FirstOrder.Language.Substructure.closure L).toFun s)
-- Mathlib.Analysis.RCLike.Inner
RCLike.conj_wInner_symm : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ)
  (f g : (i : ι) → E i), (starRingEnd 𝕜) ⟪f, g⟫_[𝕜, w] = ⟪g, f⟫_[𝕜, w]
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.MatchUnifyResult : Type
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.minKey!_modify_eq_minKey! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Raw.Const.modify t k f).minKey! = t.minKey!
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.bot_eq_top_iff_finrank_eq_one : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  ⊥ = ⊤ ↔ Module.finrank F E = 1
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.invFun_add : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {p q : Polynomial A}, PolyEquivTensor.invFun R A (p + q) = PolyEquivTensor.invFun R A p + PolyEquivTensor.invFun R A q
-- Mathlib.Topology.Order.Basic
exists_Ico_subset_of_mem_nhds' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  s ∈ nhds a → ∀ {l : α}, a < l → ∃ l' ∈ Set.Ioc a l, Set.Ico a l' ⊆ s
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeries.eq_ge_of_eq_succ : ∀ {G : Type u_1} [inst : Group G] {a b : ℕ},
  a ≤ b →
    Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G (a + 1) →
      Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G b
-- Mathlib.Logic.Equiv.Defs
Equiv.eq_symm_apply : ∀ {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : α}, y = e.symm x ↔ e y = x
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_const_of_tendsto : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {f'' : α → E''} {l : Filter α} {y : E''}, Filter.Tendsto f'' l (nhds y) → ∀ {c : F''}, c ≠ 0 → f'' =O[l] fun _x => c
-- Mathlib.Data.List.DropRight
List.rdropWhile_concat : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (x : α),
  List.rdropWhile p (l ++ [x]) = if p x = true then List.rdropWhile p l else l ++ [x]
-- Lean.Elab.MutualInductive
Lean.Elab.Command.checkValidInductiveModifier : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Lean.Elab.Modifiers → m Unit
-- Mathlib.Algebra.Algebra.Spectrum.Basic
_private.Mathlib.Algebra.Algebra.Spectrum.Basic.0.AlgHom.termσ : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
/-- A choice of open cover on which `P` is satisfied if `f` satisfies the source local closure
of `P`.  -/
AlgebraicGeometry.sourceLocalClosure.cover : {W P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X Y : AlgebraicGeometry.Scheme} →
    {f : X ⟶ Y} →
      AlgebraicGeometry.sourceLocalClosure W P f →
        AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage W) X
-- Mathlib.Topology.Algebra.Group.Basic
Units.instLocallyCompactSpaceOfT1SpaceOfContinuousMul : ∀ {α : Type u} [inst : Monoid α] [inst_1 : TopologicalSpace α] [T1Space α] [ContinuousMul α] [LocallyCompactSpace α],
  LocallyCompactSpace αˣ
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `TopologicalSpace.generatedBy_mono`. -/
deltaGenerated_mono : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} {t₁ t₂ : TopologicalSpace Y},
  t₁ ≤ t₂ → TopologicalSpace.generatedBy X ≤ TopologicalSpace.generatedBy X
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_centralizer_iff : ∀ {R : Type u_1} [inst : Ring R] {s : Set R} {z : R}, z ∈ Subring.centralizer s ↔ ∀ g ∈ s, g * z = z * g
-- Mathlib.CategoryTheory.Shift.Induced
CategoryTheory.shiftFunctorZero_inv_app_obj_of_induced : ∀ {C : Type u_2} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} D] (F : CategoryTheory.Functor C D) (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D)
  (i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F)
  [inst_4 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full]
  [inst_5 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (X : C),
  (CategoryTheory.shiftFunctorZero D A).inv.app (F.obj X) =
    CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorZero C A).inv.app X)) ((i 0).inv.app X)
-- Batteries.Lean.Expr
/-- Like `getArgD` but ignores metadata.  -/
Lean.Expr.getArgD' : (e : Lean.Expr) → ℕ → Lean.Expr → optParam ℕ e.getAppNumArgs' → Lean.Expr
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.vadd_opposite_image_add_preimage' : ∀ {G : Type u_2} [inst : AddGroup G] (g : G) (h : Gᵃᵒᵖ) (s : Set G),
  (fun y => h +ᵥ y) '' (fun x => g + x) ⁻¹' s = (fun x => g + x) ⁻¹' (fun y => h +ᵥ y) '' s
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange.addEquiv_apply : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (em' : M ≃+ N)
  (g : ι →₀ M), (Finsupp.mapRange.addEquiv em') g = Finsupp.mapRange ⇑em' ⋯ g
-- Mathlib.RepresentationTheory.Tannaka
/-- The representation on `G → k` induced by multiplication on the right in `G`.  -/
TannakaDuality.FiniteGroup.rightRegular : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Representation k G (G → k)
-- Init.Data.Option.Lemmas
Option.get_ite : ∀ {α : Type u_1} {b : α} {p : Prop} {x : Decidable p} (h : (if p then some b else none).isSome = true),
  (if p then some b else none).get h = b
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.instSMulCommClass : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] {V : Type u_8} [inst_1 : Monoid R] [inst_2 : AddMonoid V]
  [inst_3 : DistribMulAction R V] {S : Type u_9} [inst_4 : Monoid S] [inst_5 : DistribMulAction S V]
  [SMulCommClass R S V], SMulCommClass R S (HahnSeries Γ V)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.cons₁.sizeOf_spec : ∀ (a : Turing.ToPartrec.Code) (a_1 : List ℕ) (a_2 : Turing.ToPartrec.Cont),
  sizeOf (Turing.ToPartrec.Cont.cons₁ a a_1 a_2) = 1 + sizeOf a + sizeOf a_1 + sizeOf a_2
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabExport : Lean.Elab.Command.CommandElab
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_restrict' : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet t → (μ.restrict t).restrict s = μ.restrict (s ∩ t)
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.infer : Lean.Meta.Grind.AttrKind
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastCpop : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (xc : aig.RefVec w)
  (x : BitVec w) (assign : α → Bool),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := xc.get idx hidx }⟧ = x.getLsbD idx) →
    ∀ (idx : ℕ) (hidx : idx < w),
      ⟦assign,
          { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpop aig xc).aig,
            ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpop aig xc).vec.get idx hidx }⟧ =
        x.cpop.getLsbD idx
-- Mathlib.RingTheory.Ideal.Operations
/-- An ideal is radical iff it is equal to its radical.  -/
Ideal.radical_eq_iff : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R}, I.radical = I ↔ I.IsRadical