mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedComm_tmul_one : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  [inst_8 : GradedMonoid.GOne ℬ] (a : DirectSum ι fun i => 𝒜 i),
  (TensorProduct.gradedComm R 𝒜 ℬ) (a ⊗ₜ[R] 1) = 1 ⊗ₜ[R] a
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.binaryCofan_isColimit_iff : ∀ {X Y : TopCat} (c : CategoryTheory.Limits.BinaryCofan X Y),
  Nonempty (CategoryTheory.Limits.IsColimit c) ↔
    Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom c.inl) ∧
      Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom c.inr) ∧
        IsCompl (Set.range ⇑(CategoryTheory.ConcreteCategory.hom c.inl))
          (Set.range ⇑(CategoryTheory.ConcreteCategory.hom c.inr))
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepSet.eq_1 : ∀ {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
  (s t : Set Ω) (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.CondIndepSet m' hm' s t μ =
    ProbabilityTheory.Kernel.IndepSet s t (ProbabilityTheory.condExpKernel μ m') (μ.trim hm')
-- Lean.Elab.Do.Basic
/-- The type of elaborators for `do` block elements.

It is ``elabTerm `(do $e; $rest) = elabDoElem e dec``, where `elabDoElem e ·` is the elaborator for
`do` element `e`, and `dec` is the `DoElemCont` describing the elaboration of the rest of the block
`rest`.
 -/
Lean.Elab.Do.DoElab : Type
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.modify_eq_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {f : β a → β a}
  {l : Std.DHashMap.Internal.AssocList α β},
  Std.DHashMap.Internal.AssocList.modify a f l = Std.DHashMap.Internal.AssocList.alter a (fun x => Option.map f x) l
-- Mathlib.Algebra.Module.Presentation.DirectSum
/-- Given `solution : ∀ (i : ι), (relations i).Solution (M i)`, this is the
canonical solution of `Relations.directSum relations` in `⨁ i, M i`.  -/
Module.Relations.Solution.directSum : {A : Type u} →
  [inst : Ring A] →
    {ι : Type w} →
      [DecidableEq ι] →
        {relations : ι → Module.Relations A} →
          {M : ι → Type v} →
            [inst_2 : (i : ι) → AddCommGroup (M i)] →
              [inst_3 : (i : ι) → Module A (M i)] →
                ((i : ι) → (relations i).Solution (M i)) →
                  (Module.Relations.directSum relations).Solution (DirectSum ι fun i => M i)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.filterMapM.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
/-- An `R`-coalgebra is a comonoid object in the category of `R`-modules.  -/
CoalgCat.toComonObj : {R : Type u} → [inst : CommRing R] → CoalgCat R → CategoryTheory.Comon (ModuleCat R)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_comap : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N' : LieSubmodule R L M'} {m : M},
  m ∈ LieSubmodule.comap f N' ↔ f m ∈ N'
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonDocumentHighlightParams.fromJson : Lean.Json → Except String Lean.Lsp.DocumentHighlightParams
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.mk_sub : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f g : CauSeq β abv),
  CauSeq.Completion.mk f - CauSeq.Completion.mk g = CauSeq.Completion.mk (f - g)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
MulMemClass.subtype.eq_1 : ∀ {M : Type u_1} {A : Type u_3} [inst : Mul M] [inst_1 : SetLike A M] [hA : MulMemClass A M] (S' : A),
  MulMemClass.subtype S' = { toFun := Subtype.val, map_mul' := ⋯ }
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.integrable : ∀ {D : Type u_4} {V : Type u_9} [inst : NormedAddCommGroup D] [inst_1 : NormedSpace ℝ D] [inst_2 : NormedAddCommGroup V]
  [inst_3 : NormedSpace ℝ V] [inst_4 : MeasurableSpace D] {μ : MeasureTheory.Measure D} [hμ : μ.HasTemperateGrowth]
  [BorelSpace D] [SecondCountableTopology D] (f : SchwartzMap D V), MeasureTheory.Integrable (⇑f) μ
-- Mathlib.Algebra.Category.Ring.Under.Basic
/-- The base change functor `A ↦ S ⊗[R] A`.  -/
CommRingCat.tensorProd : (R S : CommRingCat) → [Algebra ↑R ↑S] → CategoryTheory.Functor (CategoryTheory.Under R) (CategoryTheory.Under S)
-- Init.Sym.Simp.SimprocDSL
/-- Simplify telescope binders but not the final body.  -/
Lean.Parser.Sym.Simp.telescope : Lean.ParserDescr
-- Lean.Meta.SynthInstance
/-- Returns `true` if the `check` at `applyAbstractResult?` may have observable side effects
for `result`. The unifications performed by the check operate on expressions derived from
`result` itself, from the types (and values) of its free variables, and from constant type
schemes instantiated with `result`'s own universe levels. Thus, if no metavariable is
reachable through `result` or through the (transitive) types and values of its free
variables, every unification is between ground expressions and cannot assign anything, so
the check is redundant. Note that mere absence of metavariables in `result` is not enough:
in issue #796, the universe constraint flows through the type `E.{?v} a` of a local
instance occurring in `result`.
 -/
_private.Lean.Meta.SynthInstance.0.Lean.Meta.checkMayHaveSideEffects : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Order.Category.BddOrd
/-- The underlying `BoundedOrderHom`.  -/
BddOrd.Hom.hom' : {X Y : BddOrd} → X.Hom Y → BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd
-- Std.Data.HashMap.Raw
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.HashMap.Raw.alter : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] → [EquivBEq α] → [Hashable α] → Std.HashMap.Raw α β → α → (Option β → Option β) → Std.HashMap.Raw α β
-- Init.Prelude
/-- No value.  -/
Option.none : {α : Type u} → Option α
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α},
  (Std.ExtHashSet.ofList l).contains k = l.contains k
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_erase_eq_of_not_compare_eq_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (∀ {km : α}, t.maxKey? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).maxKey? = t.maxKey?
-- Mathlib.Data.List.Nodup
/-- **Alias** of the forward direction of `List.nodup_attach`. -/
List.Nodup.of_attach : ∀ {α : Type u} {l : List α}, l.attach.Nodup → l.Nodup
-- Mathlib.Analysis.Analytic.Linear
LinearIsometryEquiv.analyticOnNhd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F)
  (s : Set E), AnalyticOnNhd 𝕜 (⇑f) s
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.prod_injective : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (d : HNNExtension.NormalWord.TransversalPair G A B),
  Function.Injective fun w => HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord
-- Mathlib.Algebra.Module.Congruence.Defs
/-- The first isomorphism theorem for semimodules in the case of a surjective homomorphism.  -/
ModuleCon.quotientKerEquivOfSurjective : {S : Type u_2} →
  {M : Type u_3} →
    {N : Type u_4} →
      [inst : Semiring S] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module S M] →
              [inst_4 : Module S N] →
                (f : M →ₗ[S] N) →
                  Function.Surjective ⇑f → ModuleCon.Quotient M (ModuleCon.ker f.toDistribMulActionHom) ≃ₗ[S] N
-- Mathlib.Topology.MetricSpace.Isometry
/-- **Alias** of `IsometryEquiv.image_eball`. -/
IsometryEquiv.image_emetric_ball : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : α)
  (r : ENNReal), ⇑h '' Metric.eball x r = Metric.eball (h x) r
-- Mathlib.Algebra.Order.Field.Basic
sub_inv_antitoneOn_Icc_left : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α},
  b < c → AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
-- Mathlib.Algebra.Star.Basic
/-- Note that since `starMulOfComm` is reducible, `simp` can already prove this.  -/
star_id_of_comm : ∀ {R : Type u_1} [inst : CommMonoid R] {x : R}, star x = x
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandInfo : Type
-- Mathlib.Algebra.Polynomial.RuleOfSigns
/-- Sign variations of a monomial are always zero.  -/
Polynomial.signVariations_monomial : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] (d : ℕ) (c : R),
  ((Polynomial.monomial d) c).signVariations = 0
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.mclosure_preimage_le : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (s : Set N),
  AddSubsemigroup.closure (⇑f ⁻¹' s) ≤ AddSubsemigroup.comap f (AddSubsemigroup.closure s)
-- Mathlib.RingTheory.RingHom.Etale
RingHom.Etale.of_bijective : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Function.Bijective ⇑f → f.Etale
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- **Alias** of `norm_sub_sq_real`.

---

Expand the square  -/
norm_sub_pow_two_real : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * inner ℝ x y + ‖y‖ ^ 2
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_prod : ∀ {α : Type u_1} {s : Finset α} {f : α → ℝ}, (∀ x ∈ s, f x ≠ 0) → Real.log (∏ i ∈ s, f i) = ∑ i ∈ s, Real.log (f i)
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.hasDerivAt_negMulLog : ∀ {x : ℝ}, x ≠ 0 → HasDerivAt Real.negMulLog (-Real.log x - 1) x
-- Init.Data.SInt.Bitwise
Int8.shiftLeft_zero : ∀ {a : Int8}, a <<< 0 = a
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
AlgebraNorm.mk.injEq : ∀ {R : Type u_1} [inst : SeminormedCommRing R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S]
  (toRingNorm : RingNorm S) (smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x)
  (toRingNorm_1 : RingNorm S) (smul'_1 : ∀ (a : R) (x : S), toRingNorm_1.toFun (a • x) = ‖a‖ * toRingNorm_1.toFun x),
  ({ toRingNorm := toRingNorm, smul' := smul' } = { toRingNorm := toRingNorm_1, smul' := smul'_1 }) =
    (toRingNorm = toRingNorm_1)
-- Mathlib.GroupTheory.Coset.Basic
/-- The natural bijection between a left coset `g * s` and `s`.  -/
Subgroup.leftCosetEquivSubgroup : {α : Type u_1} → [inst : Group α] → {s : Subgroup α} → (g : α) → ↑(g • ↑s) ≃ ↥s
-- Mathlib.Combinatorics.Hall.Basic
/-- Given a relation such that the image of every singleton set is finite, then the image of every
finite set is finite.  -/
instFintypeElemImageCoeFinsetOfDecidableEqOfSingletonSet : {α : Type u} →
  {β : Type v} →
    [DecidableEq β] → (R : SetRel α β) → [(a : α) → Fintype ↑(R.image {a})] → (A : Finset α) → Fintype ↑(R.image ↑A)
-- Mathlib.GroupTheory.Congruence.Defs
ConGen.Rel.symm : ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {x y : M}, ConGen.Rel r x y → ConGen.Rel r y x
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.quasiIso_truncGEMap_iff : ∀ {ι : 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'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncGE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : CategoryTheory.Limits.HasZeroObject C],
  QuasiIso (HomologicalComplex.truncGEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  (∀ (x : β), p x → q x) → Filter.blimsup u f p ≤ Filter.blimsup u f q
-- Lean.Parser.Extra
/-- The parser `manyIndent(p)` is equivalent to `withPosition((colGe p)*)`. This has the effect of
parsing zero or more occurrences of `p`, where each subsequent `p` parse needs to be indented
the same or more than the first parse.

This parser has arity 1, and returns a list of the results from `p`.
`p` is "auto-grouped" if it is not arity 1.  -/
Lean.Parser.manyIndent : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.curryingIso_inv_toFunctor_obj_obj_obj : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) (Y : D),
  ((CategoryTheory.curryingIso.inv.toFunctor.obj F).obj X).obj Y = F.obj (X, Y)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.basisSet_subset_union : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι],
  IsProperLinearSet.basisSet✝ hs ⊆ IsProperLinearSet.periods✝ hs ∪ Set.range ⇑(Pi.basisFun ℕ ι)
-- Lean.Environment
Lean.ConstantKind.induct.sizeOf_spec : sizeOf Lean.ConstantKind.induct = 1
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Set.Finite.toFinset_vadd_set : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {a : α} {s : Set β} (hs : s.Finite)
  (hf : optParam (a +ᵥ s).Finite ⋯), hf.toFinset = a +ᵥ hs.toFinset
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.le_one : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} [inst_2 : Fintype X] [IsOrderedRing S]
  (s : ↑(stdSimplex S X)) (x : X), s x ≤ 1
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsInaccessible.preAleph_ord : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → Cardinal.preAleph c.ord = c
-- Mathlib.Algebra.Divisibility.Units
/-- In a commutative monoid, an element `a` divides an element `b` iff `a` divides all left
associates of `b`.  -/
IsUnit.dvd_mul_left : ∀ {α : Type u_1} [inst : CommMonoid α] {a b u : α}, IsUnit u → (a ∣ u * b ↔ a ∣ b)
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorObj_rel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).rel =
    (CategoryTheory.Subobject.pullback
            (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)).obj
        X.rel ⊓
      (CategoryTheory.Subobject.pullback
            (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)).obj
        Y.rel
-- Mathlib.Order.Partition.Basic
Partition.sUnion_eq : ∀ {α : Type u_1} {s : Set α} (P : Partition s), ⋃₀ ↑P = s
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_fn_inj : ∀ {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 ℬ]
  {f₁ f₂ : 𝒜 →ₐᵍ[R] ℬ}, ⇑f₁ = ⇑f₂ ↔ f₁ = f₂
-- Std.Data.ExtTreeMap.Lemmas
/-- Simpler variant of `getD_filter` when `LawfulEqCmp` is available.  -/
Std.ExtTreeMap.getD_filter' : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Bool} {k : α} {fallback : β},
  (Std.ExtTreeMap.filter f t).getD k fallback = (Option.filter (f k) t[k]?).getD fallback
-- Init.Prelude
/-- Returns the slice of `as` from indices `start` to `stop` (exclusive). The resulting array has size
`(min stop as.size) - start`.

If `start` is greater or equal to `stop`, the result is empty. If `stop` is greater than the size of
`as`, the size is used instead.

Examples:
 * `#[0, 1, 2, 3, 4].extract 1 3 = #[1, 2]`
 * `#[0, 1, 2, 3, 4].extract 1 30 = #[1, 2, 3, 4]`
 * `#[0, 1, 2, 3, 4].extract 0 0 = #[]`
 * `#[0, 1, 2, 3, 4].extract 2 1 = #[]`
 * `#[0, 1, 2, 3, 4].extract 2 2 = #[]`
 * `#[0, 1, 2, 3, 4].extract 2 3 = #[2]`
 * `#[0, 1, 2, 3, 4].extract 2 4 = #[2, 3]`
 -/
Array.extract : {α : Type u_1} → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → Array α
-- Mathlib.Computability.MyhillNerode
Language.leftQuotient.eq_1 : ∀ {α : Type u} (L : Language α) (x : List α), L.leftQuotient x = {y | x ++ y ∈ L}
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RciSliceData : (α : Type u) → [Ord α] → Type u
-- Mathlib.LinearAlgebra.Pi
LinearMap.coe_single : ∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (i : ι), ⇑(LinearMap.single R φ i) = Pi.single i
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.mk.sizeOf_spec : ∀ {Γ : Type u_8} {R : Type u_9} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {α : Type u_7} [inst_2 : SizeOf Γ]
  [inst_3 : SizeOf R] [inst_4 : SizeOf α] (toFun : α → HahnSeries Γ R)
  (isPWO_iUnion_support' : (⋃ a, (toFun a).support).IsPWO)
  (finite_co_support' : ∀ (g : Γ), {a | (toFun a).coeff g ≠ 0}.Finite),
  sizeOf { toFun := toFun, isPWO_iUnion_support' := isPWO_iUnion_support', finite_co_support' := finite_co_support' } =
    1
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.mk.injEq : ∀ (carrier : Type u) [str : Group carrier] (carrier_1 : Type u) (str_1 : Group carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f}
  (hom hom_1 : (i : ι) → D₁.obj i ⟶ D₂.obj i) (e_hom : hom = hom_1)
  (comm :
    ∀ (i₁ i₂ : ι),
      CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
          ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom i₂))) =
        CategoryTheory.CategoryStruct.comp (hom i₁) (D₂.hom i₁ i₂)),
  { hom := hom, comm := comm } = { hom := hom_1, comm := ⋯ }
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- Any two objects in a codiscrete category are isomorphic.  -/
CategoryTheory.Codiscrete.iso : {A : Type u} → (x y : CategoryTheory.Codiscrete A) → x ≅ y
-- Aesop.Rule
Aesop.RegularRule.unsafe : Aesop.UnsafeRule → Aesop.RegularRule
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {fallback : α}
  {hc : t.maxKeyD fallback ∈ t}, t.getKey (t.maxKeyD fallback) hc = t.maxKeyD fallback
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.mulRingNormClass : ∀ {R : Type u_1} [inst : NonAssocRing R], MulRingNormClass (MulRingNorm R) R ℝ
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- The Coxeter matrix of type H₃.

The corresponding Coxeter-Dynkin diagram is:
```
       5
    o --- o --- o
```
 -/
CoxeterMatrix.H₃ : CoxeterMatrix (Fin 3)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β k}, k ∈ t₂ → (t₁ \ t₂).getD k fallback = fallback
-- Batteries.Recycling.RBTree.WF
/-- The `balRight` function preserves the ordering invariants.  -/
RBTree.RBNode.Ordered.balRight : ∀ {α : Type u_1} {cmp : α → α → Ordering} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp x v) l →
    RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp v x) r →
      RBTree.RBNode.Ordered cmp l → RBTree.RBNode.Ordered cmp r → RBTree.RBNode.Ordered cmp (l.balRight v r)
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_const_mul_left : ∀ {α : Type u_1} {F : Type u_4} {𝕜 : Type u_14} [inst : Norm F] [inst_1 : NormedField 𝕜] {g : α → F} {l : Filter α}
  {c : 𝕜} {f : α → 𝕜}, c ≠ 0 → ((fun x => c * f x) =Θ[l] g ↔ f =Θ[l] g)
-- Lean.Data.Json.FromToJson.Basic
Lean.ToJson.mk : {α : Type u} → (α → Lean.Json) → Lean.ToJson α
-- Mathlib.Data.Real.Basic
Real.mk_eq : ∀ {f g : CauSeq ℚ abs}, Real.mk f = Real.mk g ↔ f ≈ g
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.orderIsoMapComap_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {σ₂₁ : R₂ →+* R} [inst_7 : RingHomInvPair σ₁₂ σ₂₁] [inst_8 : RingHomInvPair σ₂₁ σ₁₂]
  (f : M ≃ₛₗ[σ₁₂] M₂) (p : Submodule R M), (Submodule.orderIsoMapComap f) p = Submodule.map (↑f) p
-- Mathlib.Topology.Order.LiminfLimsup
BoundedLENhdsClass.mk : ∀ {α : Type u_7} [inst : Preorder α] [inst_1 : TopologicalSpace α],
  (∀ (a : α), Filter.IsBounded (fun x1 x2 => x1 ≤ x2) (nhds a)) → BoundedLENhdsClass α
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
/-- A map from the base change of a graded algebra is the same as a map to the scalar restriction.

In category-theoretical terms, this is an adjunction between:
1. `𝒜 ↦ (𝒜 · |>.baseChange S)`, a functor from Graded `R`-Algebra to Graded `S`-Algebra; and:
2. `ℬ ↦ (ℬ · |>.restrictScalars R)`, a functor from Graded `S`-Algebra to Graded `R`-Algebra.
 -/
GradedAlgHom.liftEquiv : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      {A : Type u_4} →
        {B : Type u_5} →
          [inst : DecidableEq ι] →
            [inst_1 : AddMonoid ι] →
              [inst_2 : CommSemiring R] →
                [inst_3 : CommSemiring S] →
                  [inst_4 : Semiring A] →
                    [inst_5 : Semiring B] →
                      [inst_6 : Algebra R A] →
                        [inst_7 : Algebra S B] →
                          (𝒜 : ι → Submodule R A) →
                            (ℬ : ι → Submodule S B) →
                              [inst_8 : GradedAlgebra 𝒜] →
                                [inst_9 : GradedAlgebra ℬ] →
                                  [inst_10 : Algebra R S] →
                                    [inst_11 : Algebra R B] →
                                      [inst_12 : IsScalarTower R S B] →
                                        (𝒜 →ₐᵍ[R] fun x => Submodule.restrictScalars R (ℬ x)) ≃
                                          ((fun x => Submodule.baseChange S (𝒜 x)) →ₐᵍ[S] ℬ)
-- Mathlib.Algebra.LinearRecurrence
LinearRecurrence.mkSol.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (E : LinearRecurrence R) (init : Fin E.order → R) (x : ℕ),
  E.mkSol init x =
    if h : x < E.order then init ⟨x, h⟩
    else
      ∑ k,
        have x_1 := ⋯;
        E.coeffs k * E.mkSol init (x - E.order + ↑k)