mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Two partial equivs that have the same `source`, same `toFun` and same `invFun`, coincide.  -/
PartialEquiv.ext : ∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β},
  (∀ (x : α), ↑e x = ↑e' x) → (∀ (x : β), ↑e.symm x = ↑e'.symm x) → e.source = e'.source → e = e'
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.ofHom_injective : ∀ {X Y : Type u} [inst : AddCommGroup X] [inst_1 : AddCommGroup Y], Function.Injective fun f => AddCommGrpCat.ofHom f
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The `n`-th derivative of a function, as a multilinear map, defined inductively.  -/
iteratedFDeriv : (𝕜 : Type u) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type uE} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type uF} →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → (n : ℕ) → (E → F) → E → E [×n]→L[𝕜] F
-- Mathlib.Order.Cover
covBy_iff_lt_iff_le_right : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α}, y ⋖ x ↔ ∀ {z : α}, y < z ↔ x ≤ z
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.edist_eq_of_L2 : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)]
  (x y : PiLp 2 β), edist x y = (∑ i, edist (x.ofLp i) (y.ofLp i) ^ 2) ^ (1 / 2)
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.closedBall_eq_or_disjoint : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x y : X) (r : ℝ),
  Metric.closedBall x r = Metric.closedBall y r ∨ Disjoint (Metric.closedBall x r) (Metric.closedBall y r)
-- Std.Time.Date.Unit.Day
/-- Converts an `Offset` to an `Ordinal`.
 -/
Std.Time.Day.Offset.toOrdinal : (off : Std.Time.Day.Offset) → off.val ≥ 1 ∧ off.val ≤ 31 → Std.Time.Day.Ordinal
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageMap.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g}
  [inst_3 : SizeOf C] (map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom)
  (map_ι :
    autoParam
      (CategoryTheory.CategoryStruct.comp map (CategoryTheory.Limits.image.ι g.hom) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq))
      CategoryTheory.Limits.ImageMap.map_ι._autoParam),
  sizeOf { map := map, map_ι := map_ι } = 1 + sizeOf map + sizeOf map_ι
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Taking sub-families preserves equicontinuity at a point within a subset.  -/
EquicontinuousWithinAt.comp : ∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α]
  {F : ι → X → α} {S : Set X} {x₀ : X},
  EquicontinuousWithinAt F S x₀ → ∀ (u : κ → ι), EquicontinuousWithinAt (F ∘ u) S x₀
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
Filter.EventuallyEq.extDerivWithin_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E},
  ω₁ =ᶠ[nhdsWithin x s] ω₂ → ω₁ x = ω₂ x → extDerivWithin ω₁ s x = extDerivWithin ω₂ s x
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.hasForgetToFintype : CategoryTheory.HasForget₂ FinPartOrd FintypeCat
-- Init.Data.List.Sublist
List.eq_nil_of_sublist_nil : ∀ {α : Type u_1} {l : List α}, l.Sublist [] → l = []
-- Mathlib.CategoryTheory.Category.Cat.Limit
/-- Auxiliary definition: the limit category.  -/
CategoryTheory.Cat.HasLimits.limitConeX : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] → CategoryTheory.Functor J CategoryTheory.Cat → CategoryTheory.Cat
-- Std.Data.TreeSet.Basic
Std.TreeSet.instInhabited : {α : Type u} → {cmp : α → α → Ordering} → Inhabited (Std.TreeSet α cmp)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_eq_maxKeyD_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.maxKey! = t.maxKeyD default
-- Init.Meta.Defs
Lean.Meta.ApplyConfig.mk.injEq : ∀ (newGoals : Lean.Meta.ApplyNewGoals) (synthAssignedInstances allowSynthFailures approx : Bool)
  (newGoals_1 : Lean.Meta.ApplyNewGoals) (synthAssignedInstances_1 allowSynthFailures_1 approx_1 : Bool),
  ({ newGoals := newGoals, synthAssignedInstances := synthAssignedInstances, allowSynthFailures := allowSynthFailures,
        approx := approx } =
      { newGoals := newGoals_1, synthAssignedInstances := synthAssignedInstances_1,
        allowSynthFailures := allowSynthFailures_1, approx := approx_1 }) =
    (newGoals = newGoals_1 ∧
      synthAssignedInstances = synthAssignedInstances_1 ∧ allowSynthFailures = allowSynthFailures_1 ∧ approx = approx_1)
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.DTreeMap.Raw.entryAtIdxD : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → ℕ → (a : α) × β a → (a : α) × β a
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The "boundaries" map `S.X₁ ⟶ S.cycles`. (Note that in this homology API, we make no use
of the "image" of this morphism, which under some categorical assumptions would be a subobject
of `S.X₂` contained in `S.cycles`.)  -/
CategoryTheory.ShortComplex.toCycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasLeftHomology] → S.X₁ ⟶ S.cycles
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.IsStableUnderShift.isStableUnderShiftBy : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P : CategoryTheory.ObjectProperty C} {A : Type u_2}
  {inst_1 : AddMonoid A} {inst_2 : CategoryTheory.HasShift C A} [self : P.IsStableUnderShift A] (a : A),
  P.IsStableUnderShiftBy a
-- Mathlib.Analysis.Matrix.Order
Matrix.instNonnegSpectrumClass : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n], NonnegSpectrumClass ℝ (Matrix n n 𝕜)
-- Mathlib.Algebra.Order.Pi
Pi.one_le_mulSingle : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : DecidableEq ι] [inst_1 : (i : ι) → One (α i)]
  [inst_2 : (i : ι) → Preorder (α i)] {i : ι} {a : α i}, 1 ≤ Pi.mulSingle i a ↔ 1 ≤ a
-- Mathlib.Data.Nat.Init
/-- Induction principle deriving the next case from the `k` previous ones. Use as
```
induction n using stepInduction 3 with
| base n hn => ...
| step n ih => ...
```  -/
Nat.stepInduction : {motive : ℕ → Sort u_1} →
  (k : ℕ) →
    ((i : ℕ) → i < k → motive i) → ((n : ℕ) → ((i : ℕ) → i < k → motive (n + i)) → motive (n + k)) → (a : ℕ) → motive a
-- Init.Data.Iterators.Consumers.Access
_private.Init.Data.Iterators.Consumers.Access.0.Std.Iter.atIdxSlow?.match_1.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β)
  (motive :
    (n : ℕ) →
      ((a' : Std.Iter β) →
          (b' : ℕ) →
            InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, n⟩ →
              Option β) →
        Sort u_2)
  (recur :
    (a' : Std.Iter β) →
      (b' : ℕ) →
        InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
            (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, 0⟩ →
          Option β)
  (h_1 :
    (recur :
        (a' : Std.Iter β) →
          (b' : ℕ) →
            InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, 0⟩ →
              Option β) →
      motive 0 recur)
  (h_2 :
    (k : ℕ) →
      (recur :
          (a' : Std.Iter β) →
            (b' : ℕ) →
              InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                  (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, k + 1⟩ →
                Option β) →
        motive k.succ recur),
  (match 0, recur with
    | 0, recur => h_1 recur
    | k.succ, recur => h_2 k recur) =
    h_1 recur
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.AEEqFun.Integrable.eq_1 : ∀ {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] (f : α →ₘ[μ] ε), f.Integrable = MeasureTheory.Integrable (↑f) μ
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (Y.residueField (f x)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asFiberHom f x)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f (f x)) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)) h
-- Mathlib.Order.KrullDimension
Order.krullDim_eq_bot_iff : ∀ {α : Type u_1} [inst : Preorder α], Order.krullDim α = ⊥ ↔ IsEmpty α
-- Mathlib.Util.Export
Lean.Export.State.mk.injEq : ∀ (names : Lean.Export.Alloc Lean.Name) (levels : Lean.Export.Alloc Lean.Level) (exprs : Lean.Export.Alloc Lean.Expr)
  (defs : Std.HashSet Lean.Name) (stk : Array (Bool × Lean.Export.Entry)) (names_1 : Lean.Export.Alloc Lean.Name)
  (levels_1 : Lean.Export.Alloc Lean.Level) (exprs_1 : Lean.Export.Alloc Lean.Expr) (defs_1 : Std.HashSet Lean.Name)
  (stk_1 : Array (Bool × Lean.Export.Entry)),
  ({ names := names, levels := levels, exprs := exprs, defs := defs, stk := stk } =
      { names := names_1, levels := levels_1, exprs := exprs_1, defs := defs_1, stk := stk_1 }) =
    (names = names_1 ∧ levels = levels_1 ∧ exprs = exprs_1 ∧ defs = defs_1 ∧ stk = stk_1)
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setAverage_congr_fun : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → E},
  MeasurableSet s → (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) → ⨍ (x : α) in s, f x ∂μ = ⨍ (x : α) in s, g x ∂μ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_eq_get_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.minKey he = t.minKey?.get ⋯
-- Mathlib.SetTheory.Cardinal.Finite
Cardinal.natCast_lt_toENat_iff : ∀ {n : ℕ} {c : Cardinal.{u_3}}, ↑n < Cardinal.toENat c ↔ ↑n < c
-- Mathlib.Algebra.Algebra.Pi
/-- `AlgHom.pi` commutes with composition.  -/
AlgHom.pi_comp : ∀ {ι : Type u_1} {R : Type u_2} {A : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] {B : Type u_4} {C : Type u_5} [inst_3 : Semiring B] [inst_4 : Algebra R B]
  [inst_5 : Semiring C] [inst_6 : Algebra R C] (g : (i : ι) → C →ₐ[R] A i) (h : B →ₐ[R] C),
  (AlgHom.pi g).comp h = AlgHom.pi fun i => (g i).comp h
-- Lean.Language.Basic
Lean.Language.instToSnapshotTreeDynamicSnapshot : Lean.Language.ToSnapshotTree Lean.Language.DynamicSnapshot
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instAddCommGroupWithOne : {R : Type u_1} → [AddCommGroupWithOne R] → AddCommGroupWithOne Rᵐᵒᵖ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Return.mk.injEq : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {w : ℕ} (result : aig.ExtendingRefVecEntry w)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑result).aig) (result_1 : aig.ExtendingRefVecEntry w)
  (cache_1 : Std.Tactic.BVDecide.BVExpr.Cache (↑result_1).aig),
  ({ result := result, cache := cache } = { result := result_1, cache := cache_1 }) =
    (result = result_1 ∧ cache ≍ cache_1)
-- Init.Internal.Order.Basic
Lean.Order.FlatOrder.mk_inj : ∀ {α : Sort u} {b x y : α}, Lean.Order.FlatOrder.mk b x = Lean.Order.FlatOrder.mk b y ↔ x = y
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.fill.eq_def : ∀ {α : Type u_1} (x : RBTree.RBNode.Path α) (x_1 : RBTree.RBNode α),
  x.fill x_1 =
    match x, x_1 with
    | RBTree.RBNode.Path.root, t => t
    | RBTree.RBNode.Path.left c parent y b, a => parent.fill (RBTree.RBNode.node c a y b)
    | RBTree.RBNode.Path.right c a y parent, b => parent.fill (RBTree.RBNode.node c a y b)
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.removeNumLeadingSpaces.consumeSpaces.eq_def : ∀ (n n_1 : ℕ) {s : String} (it : s.Pos) (r : String),
  String.removeNumLeadingSpaces.consumeSpaces✝ n n_1 it r =
    match n_1 with
    | 0 => String.removeNumLeadingSpaces.saveLine✝ n it r
    | n_2.succ =>
      if h : it.IsAtEnd then r
      else
        if (it.get h == ' ' || it.get h == '\t') = true then
          String.removeNumLeadingSpaces.consumeSpaces✝ n n_2 (it.next h) r
        else String.removeNumLeadingSpaces.saveLine✝ n it r
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM_const : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] (c : 𝕜),
  (SchwartzMap.smulLeftCLM F fun x => c) = c • ContinuousLinearMap.id 𝕜 (SchwartzMap E F)
-- Mathlib.Data.Finset.Sups
/-- `s \\ t` is the finset of elements of the form `a \ b` where `a ∈ s`, `b ∈ t`.  -/
Finset.diffs : {α : Type u_2} → [DecidableEq α] → [GeneralizedBooleanAlgebra α] → Finset α → Finset α → Finset α
-- Mathlib.CategoryTheory.Functor.Flat
/-- Representably flat functors preserve finite limits.  -/
CategoryTheory.preservesFiniteLimits_of_flat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat F], CategoryTheory.Limits.PreservesFiniteLimits F
-- Mathlib.Algebra.Module.ZLattice.Basic
instIsZLatticeComap : ∀ (K : Type u_1) [inst : NormedField K] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace K F] (L : Submodule ℤ E)
  [inst_5 : DiscreteTopology ↥L] [IsZLattice K L] (e : F ≃L[K] E), IsZLattice K (ZLattice.comap K L ↑↑e)
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.below.one_mul : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  {motive : (a a_1 : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Relation F a a_1 → Prop}
  (x : MonCat.Colimits.Prequotient F), MonCat.Colimits.Relation.below ⋯
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- An arbitrarily chosen injective resolution of an object.  -/
CategoryTheory.injectiveResolution : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (Z : C) → [CategoryTheory.HasInjectiveResolution Z] → CategoryTheory.InjectiveResolution Z
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- (Semi)norm constructed from a `PreInnerProductSpace.Core` structure, defined to be the square
root of the scalar product.  -/
InnerProductSpace.Core.toNorm : {𝕜 : Type u_1} →
  {F : Type u_3} →
    [inst : RCLike 𝕜] → [inst_1 : AddCommGroup F] → [inst_2 : Module 𝕜 F] → [c : PreInnerProductSpace.Core 𝕜 F] → Norm F
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.needHeader.injEq : ∀ {dir : Std.Http.Protocol.H1.Direction} (a a_1 : ℕ),
  (Std.Http.Protocol.H1.Reader.State.needHeader a = Std.Http.Protocol.H1.Reader.State.needHeader a_1) = (a = a_1)
-- Mathlib.Algebra.MonoidAlgebra.Support
AddMonoidAlgebra.of'.eq_1 : ∀ (R : Type u_8) (M : Type u_9) [inst : Semiring R] (m : M), AddMonoidAlgebra.of' R M m = AddMonoidAlgebra.single m 1
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
BinaryTree.treesOfNumNodesEq_card_eq_catalan : ∀ (n : ℕ), (BinaryTree.treesOfNumNodesEq n).card = catalan n
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instRightCancelSemigroup : {α : Type u_1} → [RightCancelSemigroup α] → RightCancelSemigroup αᵒᵈ
-- Mathlib.LinearAlgebra.Eigenspace.Semisimple
Module.End.apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f g : Module.End R M} {μ : R} {k : ℕ∞} {m : M},
  m ∈ (f.genEigenspace μ) k → Commute f g → g.IsFinitelySemisimple → IsNilpotent (f - g) → g m = μ • m
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.instFunLike : {R : Type u_1} →
  {A : Type u_6} →
    {B : Type u_7} →
      {ι : Type u_10} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : DecidableEq ι] →
                    [inst_6 : AddMonoid ι] →
                      {𝒜 : ι → Submodule R A} →
                        {ℬ : ι → Submodule R B} →
                          [inst_7 : GradedAlgebra 𝒜] → [inst_8 : GradedAlgebra ℬ] → FunLike (𝒜 →ₐᵍ[R] ℬ) A B
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64.congr_simp : ∀ (a a_1 : ISize), a = a_1 → ∀ (h : System.Platform.numBits = 64), a.toBitVec64 h = a_1.toBitVec64 h
-- Mathlib.Algebra.Category.FGModuleCat.Limits
/-- The forgetful functor from `FGModuleCat k` to `ModuleCat k` creates all finite limits.  -/
FGModuleCat.forget₂CreatesLimit : {J : Type} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.FinCategory J] →
      {k : Type u} →
        [inst_2 : Ring k] →
          [IsNoetherianRing k] →
            (F : CategoryTheory.Functor J (FGModuleCat k)) →
              CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.degree_C_le : ∀ {R : Type u_1} [inst : Semiring R] (a : R), (LaurentPolynomial.C a).degree ≤ 0
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.mapId_inv_app : ∀ (X : TopCat) (U : TopologicalSpace.Opens ↑X), (TopologicalSpace.Opens.mapId X).inv.app U = CategoryTheory.eqToHom ⋯
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.nnnorm_mul_le_max : ∀ {S : Type u_1} [inst : SeminormedGroup S] [IsUltrametricDist S] (x y : S), ‖x * y‖₊ ≤ max ‖x‖₊ ‖y‖₊
-- Mathlib.RingTheory.Kaehler.Basic
_private.Mathlib.RingTheory.Kaehler.Basic.0.«term_𝖣_» : Lean.TrailingParserDescr
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.instBEqCall.beq : Lean.Meta.FunInd.Call → Lean.Meta.FunInd.Call → Bool
-- Std.Data.ExtTreeSet.Basic
/-- Extensional tree sets.

A tree set stores elements of a certain type in a certain order. It depends on a comparator function
that defines an ordering on the keys and provides efficient order-dependent queries, such as
retrieval of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function `cmp` should satisfy
certain laws that ensure a consistent ordering:

* If `a` is less than (or equal) to `b`, then `b` is greater than (or equal) to `a`
and vice versa (see the `OrientedCmp` typeclass).
* If `a` is less than or equal to `b` and `b` is, in turn, less than or equal to `c`, then `a`
is less than or equal to `c` (see the `TransCmp` typeclass).

Keys for which `cmp a b = Ordering.eq` are considered the same, i.e., there can be only one of them
be contained in a single tree set at the same time.

To avoid expensive copies, users should make sure that the tree set is used linearly.

Internally, the tree sets are represented as size-bounded trees, a type of self-balancing binary
search tree with efficient order statistic lookups.

In contrast to regular dependent tree maps, `Std.ExtTreeSet` offers several extensionality lemmas
and therefore has more lemmas about equality of tree sets. This doesn't affect the amount of
supported functions though: `Std.ExtTreeSet` supports all operations from `Std.TreeMap`.

In order to use most functions, a `TransCmp` instance is required. This is necessary to make sure
that the functions are congruent, i.e. equivalent tree sets as parameters produce equivalent return
values.

These tree sets contain a bundled well-formedness invariant, which means that they cannot
be used in nested inductive types. For these use cases, `Std.TreeSet.Raw` and
`Std.TreeSet.Raw.WF` unbundle the invariant from the tree set. When in doubt, prefer
`ExtTreeSet` over `TreeSet.Raw`.
 -/
Std.ExtTreeSet : (α : Type u) → autoParam (α → α → Ordering) Std.ExtTreeSet._auto_1 → Type u
-- Mathlib.Tactic.PNatToNat
Mathlib.Tactic.PNatToNat.coe_lt_coe : ∀ (m n : ℕ+), m < n ↔ ↑m < ↑n
-- Mathlib.GroupTheory.NoncommPiCoprod
Subgroup.noncommPiCoprod_mulSingle : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  {hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y} (i : ι) (y : ↥(H i)),
  (Subgroup.noncommPiCoprod hcomm) (Pi.mulSingle i y) = ↑y
-- Mathlib.LinearAlgebra.Dimension.Free
Module.finrank_dvd_finrank_right : ∀ (F : Type u) (K : Type v) (A : Type w) [inst : Semiring F] [inst_1 : Semiring K] [inst_2 : AddCommMonoid A]
  [inst_3 : Module F K] [inst_4 : Module K A] [inst_5 : Module F A] [IsScalarTower F K A] [StrongRankCondition F]
  [StrongRankCondition K] [Module.Free F K] [Module.Free K A], Module.finrank F K ∣ Module.finrank F A
-- Mathlib.GroupTheory.ArchimedeanDensely
Int.univ_addEquiv : Finset.univ = Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_2
-- Mathlib.Topology.Order.DenselyOrdered
/-- Let `s` be a dense set in a nontrivial dense linear order `α`. If `s` is a
separable space (e.g., if `α` has a second countable topology), then there exists a countable
dense subset `t ⊆ s` such that `t` does not contain bottom/top elements of `α`.  -/
Dense.exists_countable_dense_subset_no_bot_top : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [Nontrivial α] {s : Set α} [TopologicalSpace.SeparableSpace ↑s],
  Dense s → ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t
-- Mathlib.Topology.Path
Path.range_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Set.range toContinuousMap = {f | f 0 = x ∧ f 1 = y}
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_mapTermRel_id : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'}
  [inst_1 : L'.Structure M] {ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)}
  {fr : (n : ℕ) → L.Relations n → L'.Relations n} {n : ℕ} {φ : L.BoundedFormula α n} {v : α → M} {v' : β → M}
  {xs : Fin n → M},
  (∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M),
      FirstOrder.Language.Term.realize (Sum.elim v' xs) (ft n t) = FirstOrder.Language.Term.realize (Sum.elim v xs) t) →
    (∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap (fr n R) x = FirstOrder.Language.Structure.RelMap R x) →
      ((FirstOrder.Language.BoundedFormula.mapTermRel ft fr (fun x => id) φ).Realize v' xs ↔ φ.Realize v xs)
-- Mathlib.Topology.Algebra.ProperAction.Basic
properSMul_iff : ∀ (G : Type u_1) (X : Type u_2) [inst : TopologicalSpace G] [inst_1 : TopologicalSpace X] [inst_2 : Group G]
  [inst_3 : MulAction G X], ProperSMul G X ↔ IsProperMap fun gx => (gx.1 • gx.2, gx.2)
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_intCast : ∀ {R : Type u} [inst : Ring R] (n : ℤ), (↑n).natTrailingDegree = 0
-- Mathlib.Analysis.Fourier.AddCircle
fourier_add : ∀ {T : ℝ} {m n : ℤ} {x : AddCircle T}, (fourier (m + n)) x = (fourier m) x * (fourier n) x
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.isIntegral_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.IsIntegralHom f] (U : Y.Opens),
  AlgebraicGeometry.IsAffineOpen U → (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)).IsIntegral