mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instUpwardEnumerable_eq : Int64.instUpwardEnumerable = HasModel.instUpwardEnumerable✝
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumFinsuppEquivProdFinsupp_symm_apply : ∀ {α : Type u_12} {β : Type u_13} {γ : Type u_14} [inst : Zero γ] (fg : (α →₀ γ) × (β →₀ γ)),
  Finsupp.sumFinsuppEquivProdFinsupp.symm fg = fg.1.sumElim fg.2
-- Mathlib.Analysis.BoxIntegral.UnitPartition
_private.Mathlib.Analysis.BoxIntegral.UnitPartition.0.BoxIntegral.unitPartition.termL : Lean.ParserDescr
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings
/-- The restriction of scalars functor `SheafOfModules R' ⥤ SheafOfModules R`
induced by a morphism of sheaves of rings `R ⟶ R'`.  -/
SheafOfModules.restrictScalars : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R R' : CategoryTheory.Sheaf J RingCat} → (R ⟶ R') → CategoryTheory.Functor (SheafOfModules R') (SheafOfModules R)
-- Mathlib.Topology.PartitionOfUnity
/-- the supports of the underlying functions are a locally finite family of sets  -/
BumpCovering.locallyFinite' : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {s : optParam (Set X) Set.univ} (self : BumpCovering ι X s),
  LocallyFinite fun i => Function.support ⇑(self.toFun i)
-- Mathlib.Combinatorics.Quiver.SingleObj
/-- Prefunctors between two `SingleObj` quivers correspond to functions between the corresponding
arrows types.
 -/
Quiver.SingleObj.toPrefunctor : {α : Type u_1} → {β : Type u_2} → (α → β) ≃ Quiver.SingleObj α ⥤q Quiver.SingleObj β
-- Mathlib.Algebra.Lie.Basic
LieHom.coe_injective : ∀ {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₂], Function.Injective DFunLike.coe
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.isLE_shift_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) (X : C) (n a n' : ℤ),
  autoParam (a + n' = n) CategoryTheory.Triangulated.TStructure.isLE_shift_iff._auto_1 →
    (t.IsLE ((CategoryTheory.shiftFunctor C a).obj X) n' ↔ t.IsLE X n)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.ι_comp_colimitUnopIsoOpLimit_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.unop j)
      (CategoryTheory.Limits.colimitUnopIsoOpLimit F).hom =
    (CategoryTheory.Limits.limit.π F (Opposite.op j)).unop
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- The n-ary version of `Set.add_image_prod`.  -/
Set.image_finsetSum_pi : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (l : Finset ι) (S : ι → Set α),
  (fun f => ∑ i ∈ l, f i) '' (↑l).pi S = ∑ i ∈ l, S i
-- Mathlib.Logic.Nontrivial.Defs
nontrivial_of_ne : ∀ {α : Type u_1} (x y : α), x ≠ y → Nontrivial α
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.w_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} {X Y : CategoryTheory.CostructuredArrow S T} (f : X ⟶ Y) {Z : D} (h : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.map f.left) (CategoryTheory.CategoryStruct.comp Y.hom h) =
    CategoryTheory.CategoryStruct.comp X.hom h
-- Init.Data.String.PosRaw
String.Pos.Raw.lt_of_lt_of_le : ∀ {a b c : String.Pos.Raw}, a < b → b ≤ c → a < c
-- Lean.Class
Lean.instInhabitedClassState.default : Lean.ClassState
-- Mathlib.RingTheory.QuasiFinite.Basic
/-- [Stacks Tag 00PO](https://stacks.math.columbia.edu/tag/00PO) -/
Algebra.QuasiFinite.trans : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] [Algebra.QuasiFinite R S]
  [Algebra.QuasiFinite S T], Algebra.QuasiFinite R T
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) (n₀ : ℤ) {i₀ i₁ i₂ : ι} (f : i₀ ⟶ i₁) (g : i₁ ⟶ i₂) (fg : i₀ ⟶ i₂)
  (hfg : CategoryTheory.CategoryStruct.comp f g = fg),
  CategoryTheory.Limits.IsZero ((X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f)) →
    CategoryTheory.Mono ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg hfg))
-- Mathlib.Algebra.Central.Basic
Algebra.IsCentral.of_algEquiv : ∀ (K : Type u) [inst : CommSemiring K] (D D' : Type v) [inst_1 : Semiring D] [inst_2 : Algebra K D]
  [h : Algebra.IsCentral K D] [inst_3 : Semiring D'] [inst_4 : Algebra K D'] (e : D ≃ₐ[K] D'), Algebra.IsCentral K D'
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_mul_abs : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A),
  CFC.abs a * CFC.abs a = star a * a
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- Constructor for isomorphisms in the category of presheaves of modules.  -/
PresheafOfModules.isoMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {M₁ M₂ : PresheafOfModules R} →
        (app : (X : Cᵒᵖ) → M₁.obj X ≅ M₂.obj X) →
          autoParam
              (∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
                CategoryTheory.CategoryStruct.comp (M₁.map f)
                    ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y).hom) =
                  CategoryTheory.CategoryStruct.comp (app X).hom (M₂.map f))
              PresheafOfModules.isoMk._auto_1 →
            (M₁ ≅ M₂)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : Topology.CWComplex C] [T2Space X] {A : Set X} {n : ℕ},
  (∀ m ≤ n, ∀ (j : Topology.RelCWComplex.cell C m), IsClosed (A ∩ Topology.RelCWComplex.closedCell m j)) →
    ∀ (j : Topology.RelCWComplex.cell C (n + 1)), IsClosed (A ∩ Topology.RelCWComplex.cellFrontier (n + 1) j)
-- Mathlib.GroupTheory.Torsion
AddCommGroup.freeRank_ge_of_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : AddCommGroup H] [inst_2 : AddGroup.FG G]
  [inst_3 : AddGroup.FG H] (e : G →+ H), Function.Surjective ⇑e → AddCommGroup.freeRank H ≤ AddCommGroup.freeRank G
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inl_isoIsPushout_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y}
  {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : CategoryTheory.IsPushout f g inl inr)
  (h' : CategoryTheory.IsPushout f g inl' inr') {Z_1 : C} (h_1 : P ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp inl'
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPushout.isoIsPushout X Y h h').inv h_1) =
    CategoryTheory.CategoryStruct.comp inl h_1
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.range_liftQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ f.ker), (p.liftQ f h).range = f.range
-- Mathlib.Condensed.Explicit
/-- A `CondensedSet` version of `Condensed.ofSheafProfinite`.  -/
CondensedSet.ofSheafProfinite : (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) →
  [CategoryTheory.Limits.PreservesFiniteProducts F] → CategoryTheory.regularTopology.EqualizerCondition F → CondensedSet
-- Mathlib.Data.List.Chain
List.isChain_pmap_of_isChain : ∀ {α : Type u_1} {β : Type u_2} {R : α → α → Prop} {S : β → β → Prop} {p : α → Prop} {f : (a : α) → p a → β},
  (∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)) →
    ∀ {l : List α}, List.IsChain R l → ∀ (hl₂ : ∀ a ∈ l, p a), List.IsChain S (List.pmap f l hl₂)
-- Lean.Elab.DeclModifiers
/-- Flags and data added to declarations (eg docstrings, attributes, `private`, `unsafe`, `partial`, ...).  -/
Lean.Elab.Modifiers : Type
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity : ∀ {R : Type u_4} [inst : CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ ξ : Rˣ},
  IsPrimitiveRoot ζ k → ξ ∈ rootsOfUnity k R → ∃ i < k, ζ ^ i = ξ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_getKey?_eq_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, (t.getKey? a).isSome = t.contains a
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- The underlying topological space is compact.  -/
CompHausLike.is_compact : ∀ {P : TopCat → Prop} (self : CompHausLike P), CompactSpace ↑self.toTop
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_sup' : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M}
  {p p' : Submodule R M}, x ∈ p ⊔ p' ↔ ∃ y z, ↑y + ↑z = x
-- Aesop.BaseM
Aesop.instEmptyCollectionState : EmptyCollection Aesop.BaseM.State
-- Init.Data.List.Nat.Basic
_private.Init.Data.List.Nat.Basic.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
/-- The function `tan` is meromorphic in normal form on `Set.univ`.  -/
Complex.meromorphicNFOn_tan : MeromorphicNFOn Complex.tan Set.univ
-- Init.Util
withPtrAddrUnsafe : {α : Type u} → {β : Type v} → α → (k : USize → β) → (∀ (u₁ u₂ : USize), k u₁ = k u₂) → β
-- Mathlib.Data.Set.BoolIndicator
/-- `boolIndicator` maps `x` to `true` if `x ∈ s`, else to `false`  -/
Set.boolIndicator : {α : Type u_1} → Set α → α → Bool
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.toPlus_plusLift_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (J.toPlus P) (CategoryTheory.CategoryStruct.comp (J.plusLift η hQ) h) =
    CategoryTheory.CategoryStruct.comp η h
-- Mathlib.Geometry.RingedSpace.SheafedSpace
/-- The global sections, notated Gamma.
 -/
AlgebraicGeometry.SheafedSpace.Γ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (AlgebraicGeometry.SheafedSpace C)ᵒᵖ C
-- Init.Data.BitVec.Lemmas
/-- A bitvector is equal to 0#w if and only if all bits are `false`  -/
BitVec.zero_iff_eq_false : ∀ {w : ℕ} {x : BitVec w}, x = 0#w ↔ ∀ (i : ℕ), x.getLsbD i = false
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.uncurry_pre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A B : C}
  [inst_2 : CategoryTheory.Closed A] [inst_3 : CategoryTheory.Closed B] (f : B ⟶ A) (X : C),
  CategoryTheory.MonoidalClosed.uncurry ((CategoryTheory.MonoidalClosed.pre f).app X) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (A ⟹ X))
      ((CategoryTheory.ihom.ev A).app X)
-- Mathlib.Topology.Order.DenselyOrdered
interior_Iic : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMaxOrder α] {a : α}, interior (Set.Iic a) = Set.Iio a
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_const_nat : ∀ (m n : ℕ), (List.replicate m n).sum = m * n
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.map_def : ∀ {α : Type u_4} {β : Type u_5} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (f : α → β)
  (μ : MeasureTheory.Measure α),
  MeasureTheory.Measure.map f μ =
    if hf : AEMeasurable f μ then (MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ else 0
-- Mathlib.LinearAlgebra.Ray
/-- **Alias** of the reverse direction of `sameRay_neg_iff`.

---

`SameRay.neg` as an `iff`.  -/
SameRay.neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {x y : M}, SameRay R x y → SameRay R (-x) (-y)
-- Init.Data.UInt.Lemmas
UInt16.left_eq_add : ∀ {a b : UInt16}, a = a + b ↔ b = 0
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- A product of two standard Borel spaces is standard Borel.  -/
StandardBorelSpace.prod : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β] [StandardBorelSpace α]
  [StandardBorelSpace β], StandardBorelSpace (α × β)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_one : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.withDensity 1 = μ
-- Mathlib.RingTheory.PicardGroup
/-- If `f : M →ₗ[R] N` and `g : N →ₗ[R] M` where `M` and `N` are invertible `R`-modules, and `f` is
a left inverse of `g`, then in fact `f` is also the right inverse of `g`, and we promote this to
an `R`-module isomorphism.  -/
Module.Invertible.linearEquivOfLeftInverse : {R : Type u} →
  {M : Type v} →
    {N : Type u_1} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                [Module.Invertible R M] →
                  [Module.Invertible R N] → {f : M →ₗ[R] N} → {g : N →ₗ[R] M} → Function.LeftInverse ⇑f ⇑g → M ≃ₗ[R] N
-- Mathlib.Data.Set.Function
Set.EqOn.inter_preimage_eq : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β},
  Set.EqOn f₁ f₂ s → ∀ (t : Set β), s ∩ f₁ ⁻¹' t = s ∩ f₂ ⁻¹' t
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin.fieldCoe : (F : Type u_1) →
  [inst : Field F] →
    {E : Type u_2} → [inst_1 : Field E] → [inst_2 : Algebra F E] → (S : Set E) → CoeTC F ↥(IntermediateField.adjoin F S)
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.mem_vertexSet_of_mem_edgeSet : ∀ {α : Type u_1} {x : α} {e : Set α} {H : Hypergraph α}, e ∈ H.edgeSet → x ∈ e → x ∈ H.vertexSet
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- `spanSingleton x` is the fractional ideal generated by `x` if `0 ∉ S`  -/
FractionalIdeal.spanSingleton : {R : Type u_5} →
  [inst : CommRing R] →
    (S : Submonoid R) →
      {P : Type u_6} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → [IsLocalization S P] → P → FractionalIdeal S P
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.fromDFinsuppEquiv_single : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} [inst : DecidableEq ι]
  [inst_1 : Fintype ι] [inst_2 : CommSemiring R] [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)]
  [inst_4 : (i : ι) → (k : κ i) → Module R (M i k)] {N : Type u_1} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  [inst_7 : (i : ι) → DecidableEq (κ i)] (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) N)
  (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)),
  (((MultilinearMap.fromDFinsuppEquiv κ R) f) fun i => fun₀ | p i => x i) = (f p) x
-- Mathlib.Order.Disjointed
iSup_disjointed : ∀ {α : Type u_1} {ι : Type u_2} [inst : CompleteBooleanAlgebra α] [inst_1 : PartialOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] (f : ι → α), ⨆ i, disjointed f i = ⨆ i, f i
-- Lean.Meta.Tactic.Grind.Action
/-- `loop` reference implementation without `tryCatchRuntimeEx` for proving sanity checking lemmas.  -/
Lean.Meta.Grind.Action.loopRef : ℕ → Lean.Meta.Grind.Action → Lean.Meta.Grind.Action
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.IsIrreducible.mk : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [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},
  Nontrivial M →
    Nontrivial N →
      (∀ (q : Submodule R M), (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤) →
        (∀ (q : Submodule R N), (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.coreflection i)) → q ≠ ⊥ → q = ⊤) →
          P.IsIrreducible
-- Mathlib.MeasureTheory.Measure.MeasuredSets
/-- A ring of sets covering the space modulo `0` and generating the measurable space
structure is dense among measurable sets.  -/
MeasureTheory.dense_of_generateFrom_isSetRing : ∀ {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
  {C : Set (Set α)},
  MeasureTheory.IsSetRing C →
    (∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0) → mα = MeasurableSpace.generateFrom C → Dense (SetLike.coe ⁻¹' C)
-- Std.Data.TreeMap.Raw.Basic
/-- Two tree maps are equivalent in the sense of Equiv iff all the keys and values are equal.  -/
Std.TreeMap.Raw.«term_~m_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Preadditive.LeftExact
/-- A functor between preadditive categories which preserves kernels preserves all finite limits.
 -/
CategoryTheory.Functor.preservesFiniteLimits_of_preservesKernels : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteProducts C]
  [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.Limits.HasZeroObject D]
  [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F],
  CategoryTheory.Limits.PreservesFiniteLimits F
-- Lean.Data.Lsp.Extra
Lean.Lsp.instReprLineRange.repr : Lean.Lsp.LineRange → ℕ → Std.Format
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_hom_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C)
  (x : (∐ X.toFun).I),
  X.coproductIsoSelf.hom.φ x =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt X.I X.toFun).hom.φ x)
      (X.cofanPtIsoSelf.hom.φ ((CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt X.I X.toFun).hom.f x))
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The functor `ComposableArrows C (n + 1) ⥤ ComposableArrows C n` which forgets
the last arrow.  -/
CategoryTheory.ComposableArrows.δlastFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} → CategoryTheory.Functor (CategoryTheory.ComposableArrows C (n + 1)) (CategoryTheory.ComposableArrows C n)
-- Batteries.Data.Fin.Lemmas
Fin.isNone_of_isNone_findSome? : ∀ {n : ℕ} {α : Type u_1} {i : Fin n} {f : Fin n → Option α}, (Fin.findSome? f).isNone = true → (f i).isNone = true
-- Mathlib.RingTheory.Smooth.Pi
Algebra.FormallySmooth.pi_iff : ∀ {R : Type u_1} {I : Type u_2} (A : I → Type u_3) [inst : CommRing R] [inst_1 : (i : I) → CommRing (A i)]
  [inst_2 : (i : I) → Algebra R (A i)] [Finite I],
  Algebra.FormallySmooth R ((i : I) → A i) ↔ ∀ (i : I), Algebra.FormallySmooth R (A i)
-- Aesop.Tree.Data
Aesop.GoalOrigin.subgoal : Aesop.GoalOrigin
-- Mathlib.Analysis.Matrix.Spectrum
/-- The determinant of a Hermitian matrix is the product of its eigenvalues.  -/
Matrix.IsHermitian.det_eq_prod_eigenvalues : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), A.det = ∏ i, ↑(hA.eigenvalues i)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R],
  (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)).IsRightAdjoint
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.unop_inf : ∀ {G : Type u_2} [inst : AddGroup G] (S₁ S₂ : AddSubgroup Gᵃᵒᵖ), (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {hc : k ∈ t.modify k f}, (t.modify k f)[k] = f t[k]
-- Init.Data.OfScientific
Float32.exactlyRepresentablePowersOfTen.eq_1 : Float32.exactlyRepresentablePowersOfTen =
  #[Float32.ofBits 1065353216, Float32.ofBits 1092616192, Float32.ofBits 1120403456, Float32.ofBits 1148846080,
    Float32.ofBits 1176256512, Float32.ofBits 1203982336, Float32.ofBits 1232348160, Float32.ofBits 1259902592,
    Float32.ofBits 1287568416, Float32.ofBits 1315859240, Float32.ofBits 1343554297]
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prod_id_snd : ∀ (C : Type u₁) [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] (D : Type u₂)
  [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] (X : C × D),
  (CategoryTheory.CategoryStruct.id X).2 = CategoryTheory.CategoryStruct.id X.2
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.congr_arg : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] {f : M ≃* N} {x x' : M}, x = x' → f x = f x'
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.isZero_of_iff_subsingleton : ∀ {R : Type u} [inst : Ring R] {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  CategoryTheory.Limits.IsZero (ModuleCat.of R M) ↔ Subsingleton M
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_coeRingHom : ∀ {α : Type u_1} {l : Filter α} {R : Type u_5} [inst : Semiring R], ⇑(Filter.Germ.coeRingHom l) = Filter.Germ.ofFun
-- Mathlib.Analysis.Calculus.TangentCone.Real
/-- If a subset of a real vector space contains an open segment, then the direction of this
segment belongs to the tangent cone at its endpoints.  -/
mem_tangentConeAt_of_openSegment_subset : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousSMul ℝ E]
  {s : Set E} {x y : E}, openSegment ℝ x y ⊆ s → y - x ∈ tangentConeAt ℝ s x
-- Mathlib.Algebra.Order.Field.Basic
inv_pow_strictAnti : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  1 < a → StrictAnti fun n => (a ^ n)⁻¹
-- Mathlib.Order.RelClasses
IsPreorder.swap : ∀ {α : Type u} (r : α → α → Prop) [IsPreorder α r], IsPreorder α (Function.swap r)
-- Mathlib.Logic.Equiv.Prod
/-- Combine two equivalences using `PProd` in the domain and `Prod` in the codomain.  -/
Equiv.pprodProd : {α₁ : Sort u_2} → {β₁ : Sort u_5} → {α₂ : Type u_9} → {β₂ : Type u_10} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ×' β₁ ≃ α₂ × β₂
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.decidableMemPow : {α : Type u_2} →
  [inst : Monoid α] →
    {s : Set α} →
      [Fintype α] → [DecidableEq α] → [DecidablePred fun x => x ∈ s] → (n : ℕ) → DecidablePred fun x => x ∈ s ^ n