mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
Std.IterM.QuotStep.restrict : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        [inst_1 : Monad m] →
          [inst_2 : LawfulMonad m] → {it : Std.IterM m β} → { s // ∃ s', s = (↑s').bundledQuotient } → it.QuotStep
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.sub_self : ∀ {α : Type u} [inst : SubtractionMonoid α] {a : α}, IsAddUnit a → a - a = 0
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.getKeyGE?.go : {α : Type u} → {β : α → Type v} → [Ord α] → α → Option α → Std.DTreeMap.Internal.Impl α β → Option α
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid of a monoid inherits a monoid structure.  -/
Submonoid.toMonoid : {M : Type u_5} → [inst : Monoid M] → (S : Submonoid M) → Monoid ↥S
-- Mathlib.Order.Concept
Concept.extent_subset_extent_iff : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r}, c.extent ⊆ d.extent ↔ c ≤ d
-- Mathlib.Data.List.Rotate
List.isRotated_append : ∀ {α : Type u} {l l' : List α}, l ++ l' ~r l' ++ l
-- Mathlib.Algebra.Algebra.Operations
Submodule.map_unop_one : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) 1 = 1
-- Lean.KeyedDeclsAttribute
/-- safety: requires that `mkConst df.valueTypeName _` and `γ` are definitionally equal.  -/
Lean.KeyedDeclsAttribute.init : {γ : Type} →
  Lean.KeyedDeclsAttribute.Def γ →
    autoParam Lean.Name Lean.KeyedDeclsAttribute.init._auto_1 → IO (Lean.KeyedDeclsAttribute γ)
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The Ore minuend of a difference.  -/
AddOreLocalization.AddOreSet.oreMin : {R : Type u_1} → {inst : AddMonoid R} → {S : AddSubmonoid R} → [self : AddOreLocalization.AddOreSet S] → R → ↥S → R
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.monic_X_add_C : ∀ {R : Type u} [inst : Semiring R] (x : R), (Polynomial.X + Polynomial.C x).Monic
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If an object `X` is isomorphic to 0, there's no need to use choice to construct
an explicit isomorphism: the zero morphism suffices.  -/
CategoryTheory.Limits.isoOfIsIsomorphicZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [CategoryTheory.Limits.HasZeroMorphisms C] → {X : C} → CategoryTheory.IsIsomorphic X 0 → (X ≅ 0)
-- Lean.Elab.ConfigEval.Types
/-- Class for evaluation of an expression to a runtime value.
 -/
Lean.Elab.ConfigEval.EvalExpr : Type → Type
-- Lean.Util.FindExpr
Lean.Expr.FindStep.found.sizeOf_spec : sizeOf Lean.Expr.FindStep.found = 1
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_filterMapM : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {f : β → m (Option γ)}
  (it : Std.IterM Id β), (Std.IterM.filterMapM f it).toArray = Array.filterMapM f it.toArray.run
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instIsRightCancelMul : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Mul M] [IsRightCancelMul M], IsRightCancelMul (l.Germ M)
-- Init.Data.BitVec.Lemmas
BitVec.getElem?_zero_ofBool : ∀ (b : Bool), (BitVec.ofBool b)[0]? = some b
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.measurePreserving_add_right_neg : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G]
  (μ : MeasureTheory.Measure G) [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (g : G),
  MeasureTheory.MeasurePreserving (fun t => -(g + t)) μ μ
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.checkClass : Array Lean.Elab.Command.PreElabHeaderResult → Lean.Elab.TermElabM Unit
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The `finrank` of `(ι →₀ R)` is `Fintype.card ι`.  -/
Module.finrank_finsupp_self : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] {ι : Type v} [inst_2 : Fintype ι],
  Module.finrank R (ι →₀ R) = Fintype.card ι
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagInfo.mk.injEq : ∀ (lctx : Lean.LocalContext) (sources : List Lean.Meta.Grind.EMatchDiagNode) (target : Lean.Meta.Grind.EMatchDiagNode)
  (lctx_1 : Lean.LocalContext) (sources_1 : List Lean.Meta.Grind.EMatchDiagNode)
  (target_1 : Lean.Meta.Grind.EMatchDiagNode),
  ({ lctx := lctx, sources := sources, target := target } =
      { lctx := lctx_1, sources := sources_1, target := target_1 }) =
    (lctx = lctx_1 ∧ sources = sources_1 ∧ target = target_1)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- See Note [custom simps projection]  -/
ContinuousMulEquiv.Simps.symm_apply : (G : Type u) →
  [inst : TopologicalSpace G] →
    (H : Type v) → [inst_1 : TopologicalSpace H] → [inst_2 : Mul G] → [inst_3 : Mul H] → G ≃ₜ* H → H → G
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Sup.adjDecidable : (V : Type u) → (G H : SimpleGraph V) → [DecidableRel G.Adj] → [DecidableRel H.Adj] → DecidableRel (G ⊔ H).Adj
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.Precoverage.IsStableUnderBaseChange.of_preZeroHypercoverFamily_of_isClosedUnderIsomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.PreZeroHypercoverFamily C},
  (∀ {X : C}, P.property.IsClosedUnderIsomorphisms) →
    (∀ {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover Y)
        [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)],
        P.property E → P.property (CategoryTheory.PreZeroHypercover.pullback₁ f E)) →
      P.precoverage.IsStableUnderBaseChange
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.instIsZeroOrProbabilityMeasureOfNatMeasure : ∀ {α : Type u_1} {m0 : MeasurableSpace α}, MeasureTheory.IsZeroOrProbabilityMeasure 0
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.coprodCon.eq_1 : ∀ (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoid.coprodCon M N =
    sInf
      {c |
        (∀ (x y : M),
            c (FreeAddMonoid.of (Sum.inl (x + y))) (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))) ∧
          (∀ (x y : N),
              c (FreeAddMonoid.of (Sum.inr (x + y))) (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))) ∧
            c (FreeAddMonoid.of (Sum.inl 0)) 0 ∧ c (FreeAddMonoid.of (Sum.inr 0)) 0}
-- Mathlib.Order.Filter.Basic
Filter.iInf_sets_induct : ∀ {α : Type u} {ι : Sort x} {f : ι → Filter α} {s : Set α},
  s ∈ iInf f → ∀ {p : Set α → Prop}, p Set.univ → (∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)) → p s
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.card_mapAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {G' : Type u_3} [inst_1 : AddGroup G'] (e : G ≃+ G'),
  Nat.card ↥(e.mapAddSubgroup H) = Nat.card ↥H
-- Mathlib.Algebra.DirectSum.Ring
/-- A graded version of `Ring`.  -/
DirectSum.GRing : {ι : Type u_1} → (A : ι → Type u_2) → [AddMonoid ι] → [(i : ι) → AddCommGroup (A i)] → Type (max u_1 u_2)
-- Lean.DocString.Extension
/-- A sequence of parts with their absolute document nesting levels and header positions.
None of these parts may contain sub-parts.
 -/
Lean.VersoModuleDocs.Snippet.sections : Lean.VersoModuleDocs.Snippet → Array (ℕ × Lean.DeclarationRange × Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)
-- Mathlib.AlgebraicGeometry.AffineSpace
/-- `S`-morphisms into `Spec 𝔸(n; S)` are equivalent to the choice of `n` global sections.  -/
AlgebraicGeometry.AffineSpace.homOverEquiv : {n : Type u} →
  (S : AlgebraicGeometry.Scheme) →
    {X : AlgebraicGeometry.Scheme} →
      [inst : X.Over S] → { f // AlgebraicGeometry.Scheme.Hom.IsOver f S } ≃ (n → ↑(X.presheaf.obj (Opposite.op ⊤)))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {a : α} {c : ℕ},
  (Std.DHashMap.emptyWithCapacity c).get? a = none
-- Mathlib.Algebra.Algebra.Spectrum.Basic
_private.Mathlib.Algebra.Algebra.Spectrum.Basic.0.spectrum.«term↑ₐ_2» : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instMulAction : {α : Type u_1} →
  {R : Type u_6} →
    [inst : Monoid R] →
      [inst_1 : MulAction R ENNReal] →
        [IsScalarTower R ENNReal ENNReal] → {x : MeasurableSpace α} → MulAction R (MeasureTheory.Measure α)
-- Mathlib.CategoryTheory.Enriched.Basic
/-- Typecheck a `(𝟙_ W)`-shaped `W`-morphism as a morphism in `ForgetEnrichment W C`.  -/
CategoryTheory.ForgetEnrichment.homOf : {C : Type u₁} →
  (W : Type v) →
    [inst : CategoryTheory.Category.{w, v} W] →
      [inst_1 : CategoryTheory.MonoidalCategory W] →
        [inst_2 : CategoryTheory.EnrichedCategory W C] →
          {X Y : C} →
            (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ X ⟶[W] Y) →
              (CategoryTheory.ForgetEnrichment.of W X ⟶ CategoryTheory.ForgetEnrichment.of W Y)
-- Mathlib.Algebra.BigOperators.Pi
RingHom.functions_ext_iff : ∀ {I : Type u_7} [inst : DecidableEq I] {R : I → Type u_8} [inst_1 : (i : I) → NonAssocSemiring (R i)] [Finite I]
  {S : Type u_9} [inst_3 : NonAssocSemiring S] {g h : ((i : I) → R i) →+* S},
  g = h ↔ ∀ (i : I) (x : R i), g (Pi.single i x) = h (Pi.single i x)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono'_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.LeftHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h).π = h.π
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.BinaryBicone.ofColimitCocone_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)} (ht : CategoryTheory.Limits.IsColimit t),
  (CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).fst =
    CategoryTheory.Limits.BinaryCofan.IsColimit.desc ht (CategoryTheory.CategoryStruct.id X) 0
-- Mathlib.Data.Finset.Sups
Finset.subset_infs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {u : Finset α} {s t : Set α},
  ↑u ⊆ s ⊼ t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' ⊼ t'
-- Mathlib.Data.List.Basic
Function.LeftInverse.list_map : ∀ {α : Type u} {β : Type v} {f : α → β} {g : β → α},
  Function.LeftInverse f g → Function.LeftInverse (List.map f) (List.map g)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → t.contains t.maxKey! = true
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- Given a `p : R[X]` and a `x : S` such that `p.eval₂ f x = 0`,
`f p.leadingCoeff * x` is integral.  -/
RingHom.isIntegralElem_leadingCoeff_mul : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (p : Polynomial R) (x : S),
  Polynomial.eval₂ f x p = 0 → f.IsIntegralElem (f p.leadingCoeff * x)
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.instLiftingCochainComplexIntDerivedCategoryQQuasiIsoUpCompHomologicalComplexMapHomologicalComplexMapDerivedCategory : {C₁ : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
    [inst_1 : CategoryTheory.Abelian C₁] →
      [inst_2 : HasDerivedCategory C₁] →
        {C₂ : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_4 : CategoryTheory.Abelian C₂] →
              [inst_5 : HasDerivedCategory C₂] →
                (F : CategoryTheory.Functor C₁ C₂) →
                  [inst_6 : F.Additive] →
                    [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F] →
                      [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] →
                        CategoryTheory.Localization.Lifting DerivedCategory.Q
                          (HomologicalComplex.quasiIso C₁ (ComplexShape.up ℤ))
                          ((F.mapHomologicalComplex (ComplexShape.up ℤ)).comp DerivedCategory.Q) F.mapDerivedCategory
-- Init.Data.SInt.Lemmas
Int8.toNat_toUInt8_of_le : ∀ {x : Int8}, 0 ≤ x → x.toUInt8.toNat = x.toNatClampNeg
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_nsmul : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddMonoid β]
  [inst_3 : ContinuousAdd β] (n : ℕ) (f : C(α, β)), ⇑(n • f) = n • ⇑f
-- Mathlib.RingTheory.Teichmuller
Perfection.mk_teichmuller₀ : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R] (x : Perfection (R ⧸ I) p),
  (Ideal.Quotient.mk I) ((Perfection.teichmuller₀ p I) x) = (Perfection.coeff (R ⧸ I) p 0) x
-- Init.Data.UInt.Bitwise
UInt8.neg_one_or : ∀ {a : UInt8}, -1 ||| a = -1
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- Right unitor as a natural isomorphism.  -/
CategoryTheory.Bicategory.rightUnitorNatIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (a b : B) →
      (CategoryTheory.Bicategory.postcomposing a b b).obj (CategoryTheory.CategoryStruct.id b) ≅
        CategoryTheory.Functor.id (a ⟶ b)
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
LieAdmissibleAlgebra.ext : ∀ {R : Type u_1} {L : Type u_2} {inst : CommRing R} {inst_1 : LieAdmissibleRing L} {x y : LieAdmissibleAlgebra R L},
  SMul.smul = SMul.smul → x = y
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
AddSubsemigroup.centralizer_le : ∀ {M : Type u_1} {S T : Set M} [inst : AddSemigroup M],
  S ⊆ T → AddSubsemigroup.centralizer T ≤ AddSubsemigroup.centralizer S
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.insert : ℕ → Nat.Internal.Linear.Var → Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
/-- **Alias** of `IsLocalHom.of_surjective`. -/
Function.Surjective.isLocalHom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [Nontrivial S] [IsLocalRing R] (f : R →+* S),
  Function.Surjective ⇑f → IsLocalHom f
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.smul_mem_pointwise_smul_iff : ∀ {M : Type u_1} {R : Type u_2} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S : Subsemiring R} {x : R}, a • x ∈ a • S ↔ x ∈ S
-- Mathlib.Order.Max
/-- **Alias** of the reverse direction of `isBot_ofDual_iff`. -/
IsTop.ofDual : ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsTop a → IsBot (OrderDual.ofDual a)
-- Init.Data.SInt.Lemmas
Int64.sub_add_cancel : ∀ (a b : Int64), a - b + b = a
-- Mathlib.Order.CompleteLattice.Basic
Function.Surjective.iSup_congr : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : SupSet α] {f : ι → α} {g : ι' → α} (h : ι → ι'),
  Function.Surjective h → (∀ (x : ι), g (h x) = f x) → ⨆ x, f x = ⨆ y, g y
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.forM_eq_forM : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → β → m PUnit.{w + 1}}, Std.TreeMap.forM f t = forM t fun a => f a.1 a.2
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The Hecke triple `(H, Δ, H)` coming from a pair `(H, Δ)` with `H ≤ Δ ≤ commensurator H`.  -/
IsHeckeTriple.of_diagonal : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} {H : Subgroup G},
  H.toSubmonoid ≤ Δ → Δ ≤ (Subgroup.Commensurable.commensurator H).toSubmonoid → IsHeckeTriple Δ H H
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.card_map_of_injective : ∀ {G : Type u_1} [inst : Group G] {H : Type u_3} [inst_1 : Group H] {K : Subgroup G} {f : G →* H},
  Function.Injective ⇑f → Nat.card ↥(Subgroup.map f K) = Nat.card ↥K
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.pos_iff : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K} {x : K}, 0 < w x ↔ x ≠ 0
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Types.instReflectsLimitsOfSizeForgetTypeFun : CategoryTheory.Limits.ReflectsLimitsOfSize.{u_1, u_2, u, u, u + 1, u + 1} (CategoryTheory.forget (Type u))
-- Mathlib.Topology.Gluing
/-- The index type `J`  -/
TopCat.GlueData.MkCore.J : TopCat.GlueData.MkCore → Type u
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- A correspondence `f : α → Set β` is upper hemicontinuous if and only if its *upper inverse*
(i.e., `u : Set β ↦ f ⁻¹' (Iic u)`, note that `f ⁻¹' (Iic u) = {x | f x ⊆ u}`) sends open sets
to open sets.  -/
upperHemicontinuous_iff_isOpen_preimage_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} [inst_1 : TopologicalSpace β],
  UpperHemicontinuous f ↔ ∀ (u : Set β), IsOpen u → IsOpen (f ⁻¹' Set.Iic u)
-- Mathlib.NumberTheory.Height.NumberField
_private.Mathlib.NumberTheory.Height.NumberField.0.NumberField.relIndex_span_span_eq_relIndex_span_span : ∀ {K : Type u_1} [inst : Field K] [NumberField K] {m n : ℕ},
  m ≠ 0 →
    n ≠ 0 →
      ∀ {a b : NumberField.RingOfIntegers K},
        ↑n * a = ↑m * b →
          (Submodule.toAddSubgroup (Ideal.span {↑m})).relIndex (Submodule.toAddSubgroup (Ideal.span {↑m, a})) =
            (Submodule.toAddSubgroup (Ideal.span {↑n})).relIndex (Submodule.toAddSubgroup (Ideal.span {↑n, b}))
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.RepresentableBy.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  (homEquiv homEquiv_1 : {X : C} → (X ⟶ Y) ≃ F.obj (Opposite.op X)) (e_homEquiv : homEquiv = homEquiv_1)
  (homEquiv_comp :
    ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y),
      homEquiv (CategoryTheory.CategoryStruct.comp f g) =
        (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (homEquiv g)),
  { homEquiv := homEquiv, homEquiv_comp := homEquiv_comp } = { homEquiv := homEquiv_1, homEquiv_comp := ⋯ }
-- Mathlib.Algebra.Divisibility.Basic
exists_eq_mul_left_of_dvd : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∃ c, b = c * a
-- Aesop.Util.Unfold
Aesop.mkUnfoldSimpContext : Lean.MetaM Lean.Meta.Simp.Context
-- Mathlib.Data.Set.FiniteExhaustion
/-- A choice of a `FiniteExhaustion` for a countable set `s`.  -/
Set.Countable.finiteExhaustion : {α : Type u_1} → {s : Set α} → s.Countable → s.FiniteExhaustion
-- Mathlib.Data.Set.Disjoint
Set.univ_disjoint : ∀ {α : Type u} {s : Set α}, Disjoint Set.univ s ↔ s = ∅
-- Std.Http.Transport
/-- Sends a single ByteArray.
 -/
Std.Http.Internal.Mock.Server.send : Std.Http.Internal.Mock.Server → ByteArray → Std.Async.Async Unit
-- Aesop.Stats.File
Aesop.StatsFileRecord : Type
-- Mathlib.Algebra.MonoidAlgebra.Support
AddMonoidAlgebra.support_coeff_single_mul : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Add G] [inst_2 : IsLeftCancelAdd G]
  (f : AddMonoidAlgebra k G) (r : k),
  (∀ (y : k), r * y = 0 ↔ y = 0) →
    ∀ (x : G), (AddMonoidAlgebra.single x r * f).coeff.support = Finset.map (addLeftEmbedding x) f.coeff.support
-- Mathlib.Analysis.Calculus.FDeriv.Pow
/-- Eta-expanded form of `HasFDerivAt.pow'` -/
HasFDerivAt.fun_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {f' : E →L[𝕜] 𝔸}
  {x : E},
  HasFDerivAt f f' x →
    ∀ (n : ℕ),
      HasFDerivAt (fun i => f i ^ n) (∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f') x
-- Mathlib.RingTheory.DedekindDomain.Basic
Ring.DimensionLEOne.of_ringEquiv : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [hA : Ring.DimensionLEOne A] (e : R ≃+* A),
  Ring.DimensionLEOne R
-- Mathlib.Data.Sum.Interval
Finset.sumLexLift_mono : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  {f₁ f₁' : α₁ → β₁ → Finset γ₁} {f₂ f₂' : α₂ → β₂ → Finset γ₂} {g₁ g₁' : α₁ → β₂ → Finset γ₁}
  {g₂ g₂' : α₁ → β₂ → Finset γ₂},
  (∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b) →
    (∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b) →
      (∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b) →
        (∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b) →
          ∀ (a : α₁ ⊕ α₂) (b : β₁ ⊕ β₂), Finset.sumLexLift f₁ f₂ g₁ g₂ a b ⊆ Finset.sumLexLift f₁' f₂' g₁' g₂' a b
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.lTensor_zpow : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : N ≃ₗ[R] N) (n : ℤ),
  LinearEquiv.lTensor M f ^ n = LinearEquiv.lTensor M (f ^ n)
-- Lean.Data.Lsp.Basic
Lean.Lsp.RenameFile.oldUri : Lean.Lsp.RenameFile → Lean.Lsp.DocumentUri
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.toInt'.toIntOfNat : Lean.Expr → ℕ → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Lean.Expr × Lean.Expr)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot : ∀ {ι : Type u_1} [inst : Fintype ι] {c : NNReal} (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι)
  (π₀ : BoxIntegral.Prepartition I),
  π₀.distortion ≤ c → π₀.compl.distortion ≤ c → (l.toFilterDistortioniUnion I c π₀).NeBot
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k fallback : α},
  (List.map Prod.fst l).contains k = false → (Std.DHashMap.Raw.Const.ofList l).getKeyD k fallback = fallback
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.minD_insert_le_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  (cmp ((t.insert k).minD fallback) k).isLE = true
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_one : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S), Polynomial.map f 1 = 1
-- Mathlib.Data.ENat.Basic
ENat.toNat_le_of_le_natCast : ∀ {m : ℕ∞} {n : ℕ}, m ≤ ↑n → m.toNat ≤ n
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.preOmega_le_omega : ∀ (o : Ordinal.{u_1}), Ordinal.preOmega o ≤ Ordinal.omega o
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.foldr_eq_foldr_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → δ → δ} {init : δ},
  Std.ExtDTreeMap.foldr f init t = List.foldr (fun a b => f a.1 a.2 b) init (Std.ExtDTreeMap.Const.toList t)
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right : ∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] (A : CategoryTheory.Under R),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr A.hom (CommRingCat.ofHom (algebraMap ↑R ↑S)))
      (CategoryTheory.Under.Hom.right (CommRingCat.tensorProdObjIsoPushoutObj S A).inv) =
    CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tan.eq_1 : ∀ (z : ℂ), Complex.tan z = Complex.sin z / Complex.cos z
-- Mathlib.Data.Rat.BigOperators
Rat.cast_list_sum : ∀ {α : Type u_2} [inst : DivisionRing α] [CharZero α] (s : List ℚ), ↑s.sum = (List.map Rat.cast s).sum
-- Init.Data.Range.Polymorphic.PRange
/-- The intersection operator.  -/
Std.Roc.HasRcoIntersection.intersection : {α : Type w} → [self : Std.Roc.HasRcoIntersection α] → Std.Roc α → Std.Rco α → Std.Rco α
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.isSupported_of_iso : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (e' : K ≅ L) (e : c.Embedding c') [K.IsSupported e], L.IsSupported e
-- Lean.Util.PtrSet
Lean.PtrMap.contains : {α β : Type} → Lean.PtrMap α β → α → Bool