mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.map_p₂_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] {Z : D} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ hf₁ f₂ f₃))
      (CategoryTheory.CategoryStruct.comp f₂ h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.relativelyRepresentable.pullback₃.π hf₁ f₂ f₃) h
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_eq_getElem! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {a : α} {h' : a ∈ t}, t[a] = t[a]!
-- Mathlib.Order.Hom.Lattice
InfHom.id_apply : ∀ {α : Type u_2} [inst : Min α] (a : α), (InfHom.id α) a = a
-- Mathlib.Order.CompleteLattice.Basic
sInf_eq_top' : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sInf s = ⊤ ↔ s = ∅ ∨ s = {⊤}
-- Mathlib.RingTheory.Spectrum.Maximal.Defs
MaximalSpectrum.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : SizeOf R] (asIdeal : Ideal R) (isMaximal : asIdeal.IsMaximal),
  sizeOf { asIdeal := asIdeal, isMaximal := isMaximal } = 1 + sizeOf asIdeal + sizeOf isMaximal
-- Mathlib.Data.Matrix.Basis
Matrix.single_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α] (i : m)
  (j : n), Matrix.single i j 0 = 0
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.ofList_vadd : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : List α) (b : β), FreeAddMonoid.ofList l +ᵥ b = List.foldr f b l
-- Mathlib.Algebra.Algebra.RestrictScalars
/-- We temporarily install an action of the original ring on `RestrictScalars R S M`.  -/
RestrictScalars.moduleOrig : (R : Type u_1) →
  (S : Type u_2) →
    (M : Type u_3) →
      [inst : Semiring S] → [inst_1 : AddCommMonoid M] → [I : Module S M] → Module S (RestrictScalars R S M)
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.AddSemigrp.Hom.mk.sizeOf_spec : ∀ {A B : AddSemigrp} (hom' : ↑A →ₙ+ ↑B), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.vadd_def : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst_1 : SetLike S M] [hS : VAddMemClass S R M] (s : S)
  (r : R) (x : ↥s), r +ᵥ x = ⟨r +ᵥ ↑x, ⋯⟩
-- Lean.Parser.Command
/-- `#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.

* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
  to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
  Users can define `MonadEval` instances to extend the list of supported monads.

The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.

Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.

Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
  usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
  when there is no other way to print the result.

See also: `#reduce e` for evaluation by term reduction.
 -/
Lean.Parser.Command.evalBang : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
/-- If `f : X ⟶ Y` and `g : Y ⟶ Z` are composable morphisms,
this is the morphism `Y ⊞ Z ⟶ cokernel (f ≫ g)` which
"sends `(y, z)` to `[g(y)] + [z]`".  -/
CategoryTheory.kernelCokernelCompSequence.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y Z : C} →
        (f : X ⟶ Y) → (g : Y ⟶ Z) → Y ⊞ Z ⟶ CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp f g)
-- Std.Time.Notation.Spec
/-- Syntax for defining a date spec at compile time.
 -/
Std.Time.«termDatespec(_)» : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Pochhammer
_private.Mathlib.Analysis.SpecialFunctions.Pochhammer.0.convexOn_piecewise_Ici_descPochhammer_eval_zero : ∀ {n : ℕ},
  n ≠ 0 → ConvexOn ℝ Set.univ ((Set.Ici (↑n - 1)).piecewise (fun x => Polynomial.eval x (descPochhammer ℝ n)) 0)
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnits_strictMono : ∀ {M : Type u_1} [inst : Monoid M], StrictMono Subgroup.ofUnits
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.apply_symm_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) (v : W), φ (φ.symm v) = v
-- Mathlib.Data.Stream.Init
Stream'.map_id : ∀ {α : Type u} (s : Stream' α), Stream'.map id s = s
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_le_aleph0 : ∀ {α : Type u} [Countable α], Cardinal.mk α ≤ Cardinal.aleph0
-- Lean.Meta.Basic
/-- When `quasiPatternApprox` is set to true, we ignore condition 2.
 -/
Lean.Meta.Config.quasiPatternApprox : Lean.Meta.Config → Bool
-- Mathlib.Analysis.Calculus.ContDiff.Comp
contDiffWithinAt_prod_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {x : E} {n : WithTop ℕ∞} (f : E → F × G),
  ContDiffWithinAt 𝕜 n f s x ↔ ContDiffWithinAt 𝕜 n (Prod.fst ∘ f) s x ∧ ContDiffWithinAt 𝕜 n (Prod.snd ∘ f) s x
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.toOplax_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  F.toOplax.mapComp f g = (F.mapComp f g).hom
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.instNeg : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [NegMemClass σ A] → {𝒜 : ι → σ} → (x : Submonoid A) → Neg (HomogeneousLocalization.NumDenSameDeg 𝒜 x)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.simp.inj : ∀ {k₁ : ℤ} {c₁ : Lean.Meta.Grind.Arith.CommRing.EqCnstr} {k₂ : ℤ} {m₂ : Lean.Grind.CommRing.Mon}
  {c₂ : Lean.Meta.Grind.Arith.CommRing.EqCnstr} {k₁_1 : ℤ} {c₁_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr} {k₂_1 : ℤ}
  {m₂_1 : Lean.Grind.CommRing.Mon} {c₂_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr},
  Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.simp k₁ c₁ k₂ m₂ c₂ =
      Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.simp k₁_1 c₁_1 k₂_1 m₂_1 c₂_1 →
    k₁ = k₁_1 ∧ c₁ = c₁_1 ∧ k₂ = k₂_1 ∧ m₂ = m₂_1 ∧ c₂ = c₂_1
-- Mathlib.Order.CompletePartialOrder
CompletePartialOrder.toSupSet : {α : Type u_4} → [self : CompletePartialOrder α] → SupSet α
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.instCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          CategoryTheory.Category.{max (max (u + 1) u_2) v_1, max (max (max (u + 1) u_2) u_1) v_1}
            (TopPair.HomologyPretheory C c)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.one_le_convexBodyLTFactor : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], 1 ≤ NumberField.mixedEmbedding.convexBodyLTFactor K
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pushoutIsoOpPullback_inr_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f g] {Z_1 : Cᵒᵖ}
  (h : Opposite.op (CategoryTheory.Limits.pullback f.unop g.unop) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutIsoOpPullback f g).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f.unop g.unop).op h
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
commutative_of_addCyclic_center_quotient : ∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] [IsAddCyclic G'] (f : G →+ G'),
  f.ker ≤ AddSubgroup.center G → ∀ (a b : G), a + b = b + a
-- Mathlib.Algebra.Ring.ULift
ULift.addGroupWithOne : {R : Type u} → [AddGroupWithOne R] → AddGroupWithOne (ULift.{u_1, u} R)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
CategoryTheory.Limits.PreservesFiniteLimits.overPost : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesFiniteLimits F],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Over.post F)
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_add : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : DecidableEq o]
  [inst_1 : AddZeroClass α] (M N : (i : o) → Matrix (m' i) (n' i) α),
  Matrix.blockDiagonal' (M + N) = Matrix.blockDiagonal' M + Matrix.blockDiagonal' N
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.not_dvd_den_vonStaudt_sum : ∀ {k p : ℕ}, k > 0 → ∀ [Fact (Nat.Prime p)], ¬p ∣ (bernoulli (2 * k) + ∑ q ∈ Bernoulli.vonStaudtPrimes✝ k, 1 / ↑q).den
-- Mathlib.GroupTheory.Congruence.Defs
AddConGen.Rel.below.trans : ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {motive : (a a_1 : M) → AddConGen.Rel r a a_1 → Prop} {x y z : M}
  (a : AddConGen.Rel r x y) (a_1 : AddConGen.Rel r y z),
  AddConGen.Rel.below a → motive x y a → AddConGen.Rel.below a_1 → motive y z a_1 → AddConGen.Rel.below ⋯
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_of_contains_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → Bool}
  {k : α}, (Std.TreeMap.filter f t).contains k = true → t.contains k = true
-- Init.Tactics
/-- `rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 -/
Lean.Parser.Tactic.rwSeq : Lean.ParserDescr
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instInvolutiveInv.eq_1 : ∀ {α : Type u_1} [inst : InvolutiveInv α], Lex.instInvolutiveInv = { toInv := Lex.instInv, inv_inv := ⋯ }
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.ι_φ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) {Z_1 : C} (h : Y ⊞ Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.ι f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.φ f g) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.npow_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → Monoid (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] (i : ι)
  (x : G i) (n : ℕ), ⟦⟨i, x⟩⟧ ^ n = ⟦⟨i, x ^ n⟩⟧
-- Mathlib.Order.BooleanAlgebra.Set
Set.mem_compl : ∀ {α : Type u_1} {s : Set α} {x : α}, x ∉ s → x ∈ sᶜ
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
_private.Mathlib.GroupTheory.SpecificGroups.Quaternion.0.instDecidableEqQuaternionGroup.decEq.match_1.eq_3 : ∀ {n : ℕ} (motive : QuaternionGroup n → QuaternionGroup n → Sort u_1) (a a_1 : ZMod (2 * n))
  (h_1 : (a b : ZMod (2 * n)) → motive (QuaternionGroup.a a) (QuaternionGroup.a b))
  (h_2 : (a a_2 : ZMod (2 * n)) → motive (QuaternionGroup.a a) (QuaternionGroup.xa a_2))
  (h_3 : (a a_2 : ZMod (2 * n)) → motive (QuaternionGroup.xa a) (QuaternionGroup.a a_2))
  (h_4 : (a b : ZMod (2 * n)) → motive (QuaternionGroup.xa a) (QuaternionGroup.xa b)),
  (match QuaternionGroup.xa a, QuaternionGroup.a a_1 with
    | QuaternionGroup.a a, QuaternionGroup.a b => h_1 a b
    | QuaternionGroup.a a, QuaternionGroup.xa a_2 => h_2 a a_2
    | QuaternionGroup.xa a, QuaternionGroup.a a_2 => h_3 a a_2
    | QuaternionGroup.xa a, QuaternionGroup.xa b => h_4 a b) =
    h_3 a a_1
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.subset_zeroLocus_vanishingIdeal : ∀ {R : Type u} [inst : CommSemiring R] (t : Set (PrimeSpectrum R)),
  t ⊆ PrimeSpectrum.zeroLocus ↑(PrimeSpectrum.vanishingIdeal t)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instNeg : {A : Type u_1} →
  {G : Type u_2} →
    [inst : Semiring A] →
      [inst_1 : Monoid G] →
        {V : Type u_6} →
          {W : Type u_7} →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommGroup W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → Neg (ρ.IntertwiningMap σ)
-- Mathlib.Topology.Order.Real
ENNReal.instOrderTopology : OrderTopology ENNReal
-- Std.Async.System
_private.Std.Async.System.0.Std.Async.System.Environment.mk.inj : ∀ {toHashMap toHashMap_1 : Std.HashMap String String},
  { toHashMap := toHashMap } = { toHashMap := toHashMap_1 } → toHashMap = toHashMap_1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)},
  List.Pairwise (fun a b => (a.1 == b.1) = false) l →
    (∀ a ∈ m, (List.map Prod.fst l).contains a = false) →
      (Std.ExtDHashMap.Const.insertMany m l).size = m.size + l.length
-- Mathlib.CategoryTheory.Shift.InducedShiftSequence
/-- Given an isomorphism of functors `e : L ⋙ F ≅ G` relating functors `L : C ⥤ D`,
`F : D ⥤ A` and `G : C ⥤ A`, an additive monoid `M`, a family of functors `F' : M → D ⥤ A`
equipped with isomorphisms `e' : ∀ m, L ⋙ F' m ≅ G.shift m`, this is the shift sequence
induced on `F` induced by a shift sequence for the functor `G`, provided that
the functor `(whiskeringLeft C D A).obj L` of precomposition by `L` is fully faithful.  -/
CategoryTheory.Functor.ShiftSequence.induced : {C : Type u_1} →
  {D : Type u_2} →
    {A : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} A] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor D A} →
                {G : CategoryTheory.Functor C A} →
                  (L.comp F ≅ G) →
                    (M : Type u_4) →
                      [inst_3 : AddMonoid M] →
                        [inst_4 : CategoryTheory.HasShift C M] →
                          [inst_5 : G.ShiftSequence M] →
                            (F' : M → CategoryTheory.Functor D A) →
                              ((m : M) → L.comp (F' m) ≅ G.shift m) →
                                [((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Full] →
                                  [((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Faithful] →
                                    [inst_8 : CategoryTheory.HasShift D M] → [L.CommShift M] → F.ShiftSequence M
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isEmpty_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  (Std.DTreeMap.Raw.Const.toArray t).isEmpty = t.isEmpty
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_inv : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F],
  (CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp L W F G).εIso.inv =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.LaxMonoidal.ε L))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Localization.Lifting.iso L W G F).hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.Functor.OplaxMonoidal.η G))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.foldl_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} {δ : Type w} [Std.TransCmp cmp]
  {f : δ → α → β → δ} {init : δ}, t₁.Equiv t₂ → Std.TreeMap.foldl f init t₁ = Std.TreeMap.foldl f init t₂
-- Init.Data.Rat.Basic
Rat.instNeg : Neg ℚ
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- A family of continuous linear maps is continuous within `s` at `x` iff all its applications
are.  -/
continuousWithinAt_clm_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  {X : Type u_1} [inst_6 : TopologicalSpace X] [FiniteDimensional 𝕜 E] {f : X → E →L[𝕜] F} {s : Set X} {x : X},
  ContinuousWithinAt f s x ↔ ∀ (y : E), ContinuousWithinAt (fun q => (f q) y) s x
-- Lean.Elab.DeclModifiers
/-- Retrieve doc string from `stx` of the form `(docComment)?`.
 -/
Lean.Elab.expandOptDocComment? : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Lean.Syntax → m (Option String)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.comp_smulₛₗ : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {M : Type u_6} [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M] [inst_5 : Module R M] {M₂ : Type u_7}
  [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] {M₃ : Type u_8}
  [inst_9 : TopologicalSpace M₃] [inst_10 : AddCommMonoid M₃] [inst_11 : Module R₃ M₃] {σ₁₂ : R →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_13 : SMulCommClass R₂ R₂ M₂]
  [inst_14 : SMulCommClass R₃ R₃ M₃] [inst_15 : ContinuousConstSMul R₂ M₂] [inst_16 : ContinuousConstSMul R₃ M₃]
  (h : M₂ →SL[σ₂₃] M₃) (c : R₂) (f : M →SL[σ₁₂] M₂), h ∘SL (c • f) = σ₂₃ c • h ∘SL f
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_congr : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  f =ᵐ[μ] g → ⨍⁻ (x : α), f x ∂μ = ⨍⁻ (x : α), g x ∂μ
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.coe_zero : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Zero 𝕜] [inst_1 : LE α], ⇑0 = 0
-- Init.Data.Int.DivMod.Lemmas
Int.mul_bmod : ∀ (a b : ℤ) (n : ℕ), (a * b).bmod n = (a.bmod n * b.bmod n).bmod n
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.isIso_rightHomologyMap_of_iso : ∀ {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₂) [CategoryTheory.IsIso φ] [inst_3 : S₁.HasRightHomology]
  [inst_4 : S₂.HasRightHomology], CategoryTheory.IsIso (CategoryTheory.ShortComplex.rightHomologyMap φ)
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapWhiskerRight_app : ∀ {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] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] {Fₗ Gₗ : CategoryTheory.Functor C E} (α : Fₗ ⟶ Gₗ)
  (H : CategoryTheory.Functor D E') (x : CategoryTheory.Join C D),
  (CategoryTheory.Join.mapWhiskerRight α H).app x =
    match x with
    | CategoryTheory.Join.left x => (CategoryTheory.Join.inclLeft E E').map (α.app x)
    | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right (H.obj x))
-- Mathlib.Order.Interval.Finset.Defs
Set.instFintypeIco : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → (a b : α) → Fintype ↑(Set.Ico a b)
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.Exception : Type
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ResidueField.map_algebraMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (I : Ideal R) [inst_2 : I.IsPrime]
  (J : Ideal S) [inst_3 : J.IsPrime] (f : R →+* S) (hf : I = Ideal.comap f J) (r : R),
  (Ideal.ResidueField.map I J f hf) ((algebraMap R I.ResidueField) r) = (algebraMap S J.ResidueField) (f r)
-- Batteries.Control.Nondet.Basic
/-- Convert a monadic optional value to a nondeterministic value.  -/
Nondet.ofOptionM : {σ : Type} → {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α : Type} → m (Option α) → Nondet m α
-- Init.Data.UInt.Lemmas
UInt32.ofNat_usizeSize_sub_one : UInt32.ofNat (USize.size - 1) = 4294967295
-- Init.Control.Lawful.Lemmas
map_inj_of_left_inverse : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Functor m] [LawfulFunctor m] {f : α → β},
  (∃ g, ∀ (x : α), g (f x) = x) → ∀ {x y : m α}, f <$> x = f <$> y ↔ x = y
-- Init.Data.List.Lemmas
List.append_ne_nil_of_left_ne_nil : ∀ {α : Type u_1} {s : List α}, s ≠ [] → ∀ (t : List α), s ++ t ≠ []
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
/-- If `M` multiplicatively acts on `α`, then `DomMulAct M` acts on `α → β` as well as some
bundled maps from `α`. This is a type synonym for `MulOpposite M`, so this corresponds to a right
action of `M`.  -/
«term_ᵈᵐᵃ» : Lean.TrailingParserDescr
-- Lean.Meta.ArgsPacker
/-- Iterated `PSigma.casesOn`:
Given `e : a ⊗' b ⊗' …` (where `e` is `FVarId`), a type `codomain[e]` of level `u`, and
`alt : (x : a) → (y : b) → … → codomain`, uses `PSigma.casesOn` to invoke `alt` on `e`.
 -/
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Unary.casesOn : List Lean.Name → Lean.Expr → Lean.Level → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.LocalProperties.Projective
/-- Also see `IsLocalizedModule.lift_rank_eq` for a version for non-free modules,
but requires `S` to not contain any zero-divisors.
 -/
Module.lift_rank_of_isLocalizedModule_of_free : ∀ {R : Type u_1} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (Rₛ : Type uR')
  {Mₛ : Type uM'} [inst_3 : AddCommGroup Mₛ] [inst_4 : Module R Mₛ] [inst_5 : CommRing Rₛ] [inst_6 : Algebra R Rₛ]
  [inst_7 : Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (S : Submonoid R) (f : M →ₗ[R] Mₛ) [IsLocalization S Rₛ]
  [IsLocalizedModule S f] [Module.Free R M] [Nontrivial Rₛ],
  Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{uM', uM} (Module.rank R M)