mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Linear
/-- `p.div k` divides all coefficients of the polynomial `p` by `k`, but
rounds up the constant using `cdiv`.
Notes:
- We only use this function with `k`s that divides all coefficients.
- We use `cdiv` for the constant to implement the inequality tightening rule.
 -/
Int.Internal.Linear.Poly.div : ℤ → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly
-- Std.Http.Transport
/-- Sends ByteArrays through a channel.
 -/
Std.Http.Internal.Mock.sendAll : Std.CloseableChannel ByteArray → Array ByteArray → Std.Async.Async Unit
-- Aesop.BaseM
Aesop.BaseM.instInhabitedState : Inhabited Aesop.BaseM.State
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.isNextOutParamOfLocalInstanceAndResult.isOutParamOfLocalInstance : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.epi_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f],
  CategoryTheory.Epi f
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitCoyonedaHomIsoLimit'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (D : CategoryTheory.Functor I C) (F : CategoryTheory.Functor C (Type u₂))
  [inst_2 : CategoryTheory.Limits.HasColimit (D.op.comp CategoryTheory.coyoneda)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))],
  CategoryTheory.Limits.colimitCoyonedaHomIsoLimit' D F =
    CategoryTheory.Limits.colimitHomIsoLimitYoneda' (D.op.comp CategoryTheory.coyoneda) F ≪≫
      CategoryTheory.Limits.HasLimit.isoOfNatIso
        ((D.comp (CategoryTheory.Prod.sectL C F)).isoWhiskerLeft (CategoryTheory.coyonedaLemma C))
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoid.End.instAddCommGroup : {M : Type uM} → [inst : AddCommGroup M] → AddCommGroup (AddMonoid.End M)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringRightObjCompIso_hom_app_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] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D')
  (X : CategoryTheory.Functor E C) (X_1 : E),
  ((F.whiskeringRightObjCompIso G).hom.app X).app X_1 = CategoryTheory.CategoryStruct.id (G.obj (F.obj (X.obj X_1)))
-- Mathlib.Algebra.DirectSum.Internal
SetLike.GradeZero.algebraMap_apply : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : CommSemiring R] [inst_1 : AddMonoid ι] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : SetLike.GradedMonoid A] (x : ↥(A 0)),
  (algebraMap (↥(A 0)) R) x = ↑x
-- Mathlib.GroupTheory.Finiteness
/-- A group is finitely generated iff there exists a surjective homomorphism from a `FreeGroup`
on finitely many generators.  -/
Group.fg_iff_exists_freeGroup_hom_surjective : ∀ {G : Type u_3} [inst : Group G], Group.FG G ↔ ∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.CompletelyDistribLattice.MinimalAxioms.toCompleteDistribLattice.match_1_3.splitter : {α : Type u_1} →
  (s : Set α) →
    (motive :
        (i : ULift.{u_1, 0} Bool) →
          (match i with
            | { down := true } => PUnit.{u_1 + 1}
            | { down := false } => ↑s) →
            Sort u_2) →
      (i : ULift.{u_1, 0} Bool) →
        (j :
            match i with
            | { down := true } => PUnit.{u_1 + 1}
            | { down := false } => ↑s) →
          ((j :
                match { down := true } with
                | { down := true } => PUnit.{u_1 + 1}
                | { down := false } => ↑s) →
              motive { down := true } j) →
            ((j :
                  match { down := false } with
                  | { down := true } => PUnit.{u_1 + 1}
                  | { down := false } => ↑s) →
                motive { down := false } j) →
              motive i j
-- Batteries.Data.PairingHeap
_private.Batteries.Data.PairingHeap.0.Batteries.PairingHeapImp.Heap.foldM.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (α × Batteries.PairingHeapImp.Heap α) → Sort u_2) (h_1 : none = none → motive none)
  (h_2 : (hd : α) → (tl : Batteries.PairingHeapImp.Heap α) → none = some (hd, tl) → motive (some (hd, tl))),
  (match eq : none with
    | none => h_1 eq
    | some (hd, tl) => h_2 hd tl eq) =
    h_1 ⋯
-- Mathlib.Algebra.Module.ZLattice.Basic
Module.Basis.ofZLatticeBasis_comap : ∀ (K : Type u_1) [inst : NormedField K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  [inst_3 : HasSolidNorm K] [inst_4 : FloorRing K] {E : Type u_2} [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace K E] [inst_7 : FiniteDimensional K E] [inst_8 : ProperSpace E] {F : Type u_3}
  [inst_9 : NormedAddCommGroup F] [inst_10 : NormedSpace K F] [inst_11 : FiniteDimensional K F]
  [inst_12 : ProperSpace F] (L : Submodule ℤ E) [inst_13 : DiscreteTopology ↥L] [inst_14 : IsZLattice K L]
  (e : F ≃L[K] E) {ι : Type u_4} (b : Module.Basis ι ℤ ↥L),
  Module.Basis.ofZLatticeBasis K (ZLattice.comap K L ↑↑e) (Module.Basis.ofZLatticeComap K L (↑e) b) =
    (Module.Basis.ofZLatticeBasis K L b).map ↑e.symm
-- Init.Data.UInt.Basic
/-- Bitwise left shift for word-sized unsigned integers. Usually accessed via the `<<<` operator.

This function is overridden at runtime with an efficient implementation.
 -/
USize.shiftLeft : USize → USize → USize
-- Mathlib.Analysis.Convex.Exposed
IsExposed.refl : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] (A : Set E), IsExposed 𝕜 A A
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.leftAdjointOplaxMonoidal_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : G.LaxMonoidal],
  CategoryTheory.Functor.OplaxMonoidal.η F =
    (adj.homEquiv (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).symm
      (CategoryTheory.Functor.LaxMonoidal.ε G)
-- Mathlib.Algebra.Category.MonCat.Basic
/-- multiplicative equivalences between `Monoid`s are the same as (isomorphic to) isomorphisms
in `MonCat`  -/
mulEquivIsoMonCatIso : {X Y : Type u} → [inst : Monoid X] → [inst_1 : Monoid Y] → X ≃* Y ≅ MonCat.of X ≅ MonCat.of Y
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Preconnected.exists_adj_of_nontrivial : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} [Nontrivial ↑H.verts],
  H.Preconnected → ∀ (v : ↑H.verts), ∃ u, H.Adj (↑v) u
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.ext_ring_iff : ∀ {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  [Finite ι] {f g : MultilinearMap R (fun x => R) M₂}, f = g ↔ (f fun x => 1) = g fun x => 1
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffOn_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'},
  (∀ i ∈ t, ContDiffOn 𝕜 n (f i) s) → ContDiffOn 𝕜 n (fun y => ∏ i ∈ t, f i y) s
-- Mathlib.Analysis.Analytic.Basic
/-- `p converges to f` within `s`  -/
HasFPowerSeriesWithinOnBall.hasSum : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    ∀ {y : E}, x + y ∈ insert x s → y ∈ Metric.eball 0 r → HasSum (fun n => (p n) fun x => y) (f (x + y))
-- Mathlib.RingTheory.SimpleModule.Isotypic
isIsotypicOfType_submodule_iff : ∀ {R : Type u_2} {M : Type u} {S : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup S]
  [inst_3 : Module R M] [inst_4 : Module R S] {N : Submodule R M},
  IsIsotypicOfType R (↥N) S ↔ ∀ m ≤ N, ∀ [IsSimpleModule R ↥m], Nonempty (↥m ≃ₗ[R] S)
-- Mathlib.Order.Basic
/-- **Alias** of `lt_of_strongLT`. -/
StrongLT.lt : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → Preorder (π i)] {a b : (i : ι) → π i} [Nonempty ι],
  StrongLT a b → a < b
-- Init.Data.UInt.Bitwise
UInt16.not_eq_neg_sub : ∀ (a : UInt16), ~~~a = -a - 1
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsCofilteredForall : ∀ {α : Type w} {I : α → Type u₁} [inst : (i : α) → CategoryTheory.Category.{v₁, u₁} (I i)]
  [∀ (i : α), CategoryTheory.IsCofiltered (I i)], CategoryTheory.IsCofiltered ((i : α) → I i)
-- Mathlib.Analysis.Normed.Module.WeakDual
WeakDual.im_extendRCLikeL_apply_apply : ∀ {𝕜 : Type u_5} {F : Type u_7} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (f : WeakDual ℝ F) (x : F), RCLike.im ((WeakDual.extendRCLikeL f) x) = -f (RCLike.I • x)
-- Lean.DocString.Markdown
/-- Wraps a typed inline renderer as an `InlineMdRenderer` by decoding the `Dynamic` custom element as
`α`.
 -/
Lean.Doc.mkInlineMdRenderer : (α : Type) → [TypeName α] → Lean.Doc.InlineMdRendererOf α → Lean.Doc.InlineMdRenderer
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.inl_inr_pushoutAssoc_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂)
  (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂]
  [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂))
      g₄]
  [inst_4 :
    CategoryTheory.Limits.HasPushout g₁
      (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₃ g₄)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.inr g₁
          (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))
        (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ g₂)
      (CategoryTheory.Limits.pushout.inl
        (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
-- Mathlib.Data.Sym.Sym2
Sym2.mem_iff_mem : ∀ {α : Type u_1} {x : α} {z : Sym2 α}, Sym2.Mem x z ↔ x ∈ z
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.responseBody.inj : ∀ {β : Type} {x x_1 : Option Std.Http.Chunk},
  Std.Http.Server.Connection.Recv.responseBody✝ x = Std.Http.Server.Connection.Recv.responseBody✝ x_1 → x = x_1
-- Mathlib.Algebra.Ring.Parity
Odd.mul : ∀ {α : Type u_2} [inst : Semiring α] {a b : α}, Odd a → Odd b → Odd (a * b)
-- Mathlib.RingTheory.Unramified.Finite
KaehlerDifferential.eq_1 : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Ω[S⁄R] = (KaehlerDifferential.ideal R S).Cotangent
-- Init.Data.Vector.Lex
Vector.mk_lex_mk : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {lt : α → α → Bool} {xs ys : Array α} {n₁ : xs.size = n} {n₂ : ys.size = n},
  (Vector.mk xs n₁).lex (Vector.mk ys n₂) lt = xs.lex ys lt
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_comm : ∀ {α : Sort u_1} [inst : DecidableEq α] (a b : α), Equiv.swap a b = Equiv.swap b a
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableAt_neg_iff : ∀ {𝕜 : 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}
  {x : E}, DifferentiableAt 𝕜 (-f) x ↔ DifferentiableAt 𝕜 f x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_comp_smul : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p]
  [ContinuousMapZero.UniqueHom R A] {S : Type u_3} [inst_13 : SMulZeroClass S R] [ContinuousConstSMul S R]
  [inst_15 : SMulZeroClass S A] [IsScalarTower S R A] [IsScalarTower S R (R → R)] (s : S) (f : R → R) (a : A),
  autoParam (ContinuousOn f ((fun x => s • x) '' quasispectrum R a)) cfcₙ_comp_smul._auto_1 →
    autoParam (f 0 = 0) cfcₙ_comp_smul._auto_3 →
      autoParam (p a) cfcₙ_comp_smul._auto_5 → cfcₙ (fun x => f (s • x)) a = cfcₙ f (s • a)
-- Batteries.Data.Stream
_private.Batteries.Data.Stream.0.Std.Stream.drop.match_1.eq_2 : ∀ {σ : Type u_1} {α : Type u_2} (motive : Option (α × σ) → Sort u_3) (fst : α) (s : σ) (h_1 : Unit → motive none)
  (h_2 : (fst : α) → (s : σ) → motive (some (fst, s))),
  (match some (fst, s) with
    | none => h_1 ()
    | some (fst, s) => h_2 fst s) =
    h_2 fst s
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.skipSuffixWhile_prop_eq_skipSuffixWhile_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice},
  s.skipSuffixWhile p = s.skipSuffixWhile fun x => decide (p x)
-- Mathlib.FieldTheory.KummerPolynomial
pow_ne_of_irreducible_X_pow_sub_C : ∀ {K : Type u} [inst : Field K] {n : ℕ} {a : K},
  Irreducible (Polynomial.X ^ n - Polynomial.C a) → ∀ {m : ℕ}, m ∣ n → m ≠ 1 → ∀ (b : K), b ^ m ≠ a
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- The Gromov-Hausdorff distance defines a genuine distance on the Gromov-Hausdorff space.  -/
GromovHausdorff.instMetricSpaceGHSpace : MetricSpace GromovHausdorff.GHSpace
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.foldM_filterMapM : ∀ {α β γ δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [LawfulMonad o] [inst_8 : Std.IteratorLoop α Id n] [inst_9 : Std.IteratorLoop α Id o]
  [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o] [inst_12 : MonadLiftT n o] [LawfulMonadLiftT n o]
  {f : β → n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Std.Iter β},
  Std.IterM.foldM g init (Std.Iter.filterMapM f it) =
    Std.Iter.foldM
      (fun d b => do
        let __x ← liftM (f b)
        match __x with
          | some c => g d c
          | x => pure d)
      init it
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_bot : ∀ {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 σ₁₂] (f : M →ₛₗ[σ₁₂] M₂), Submodule.map f ⊥ = ⊥
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.postEquiv_unitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : T ≌ D),
  (CategoryTheory.Over.postEquiv X F).unitIso =
    CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Over.isoMk (F.unitIso.app A.left) ⋯) ⋯
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.hComp_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {a b : CategoryTheory.CatEnrichedOrdinary C}
  {f f' : a ⟶ b} (η : f ⟶ f'),
  CategoryTheory.CatEnrichedOrdinary.hComp η (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id b)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp η (CategoryTheory.eqToHom ⋯))
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.instHasInjectiveDimensionLTOfNatNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.HasInjectiveDimensionLT 0 0
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.RightLinear.μᵣ_comp_δᵣ : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.RightLinear C] (d : D) (c : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c)
      (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c)
-- Mathlib.Tactic.Contrapose
Mathlib.Tactic.Contrapose.contrapose₃ : ∀ {p q : Prop}, (q → ¬p) → p → ¬q
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.closure : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {A : Set E}
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E], Balanced 𝕜 A → Balanced 𝕜 (closure A)
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.hasColimitsOfShape_grothendieck : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj X)) H] [CategoryTheory.Limits.HasColimitsOfShape C H],
  CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Grothendieck F) H
-- Std.Data.TreeMap.Basic
/-- Tree maps.

A tree map stores an assignment of keys to values. 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 entry
with key either `a` or `b` in a tree map. Looking up either `a` or `b` always yields the same entry,
if any is present.

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

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

For use in proofs, the type `Std.ExtTreeMap` of extensional tree maps should be preferred. This
type comes with several extensionality lemmas and provides the same functions but requires a
`TransCmp` instance to work with.

These tree maps contain a bundled well-formedness invariant, which means that they cannot
be used in nested inductive types. For these use cases, `Std.TreeMap.Raw` and
`Std.TreeMap.Raw.WF` unbundle the invariant from the tree map. When in doubt, prefer
`TreeMap` over `TreeMap.Raw`.
 -/
Std.TreeMap : (α : Type u) → Type v → autoParam (α → α → Ordering) Std.TreeMap._auto_1 → Type (max u v)
-- Mathlib.Order.Interval.Finset.Basic
Set.Infinite.exists_lt : ∀ {α : Type u_2} [inst : LinearOrder α] [LocallyFiniteOrderTop α] {s : Set α}, s.Infinite → ∀ (a : α), ∃ b ∈ s, b < a
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The isomorphism version of `rightZigzag`.  -/
CategoryTheory.Bicategory.rightZigzagIso : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        {g : b ⟶ a} →
          (CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) →
            (CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) →
              (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id a) ≅
                CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id b) g)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.insert.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l' : Std.DTreeMap.Internal.Impl α β)
  (motive : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β l'.size (l'.size + 1) → Sort u_3)
  (d : Std.DTreeMap.Internal.Impl α β) (hd : d.Balanced) (hd₁ : l'.size ≤ d.size) (hd₂ : d.size ≤ l'.size + 1)
  (h_1 :
    (d : Std.DTreeMap.Internal.Impl α β) →
      (hd : d.Balanced) →
        (hd₁ : l'.size ≤ d.size) →
          (hd₂ : d.size ≤ l'.size + 1) →
            motive { impl := d, balanced_impl := hd, lb_le_size_impl := hd₁, size_impl_le_ub := hd₂ }),
  (match { impl := d, balanced_impl := hd, lb_le_size_impl := hd₁, size_impl_le_ub := hd₂ } with
    | { impl := d, balanced_impl := hd, lb_le_size_impl := hd₁, size_impl_le_ub := hd₂ } => h_1 d hd hd₁ hd₂) =
    h_1 d hd hd₁ hd₂
-- Mathlib.RingTheory.Norm.Defs
/-- If `x` is in the base ring `R` and `S` is free over `R`, then the norm is `x ^ [S : R]`.

(If `S` is not finitely generated over `R`, then `norm = 1 = x ^ 0 = x ^ (finrank R S)`.)
 -/
Algebra.norm_algebraMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [Module.Free R S] (x : R),
  (Algebra.norm R) ((algebraMap R S) x) = x ^ Module.finrank R S
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getD.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (fallback : β k) (size : ℕ) (k' : α)
  (v : β k') (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k' v l r).getD k fallback =
    match h : compare k k' with
    | Ordering.lt => l.getD k fallback
    | Ordering.gt => r.getD k fallback
    | Ordering.eq => cast ⋯ v
-- Mathlib.LinearAlgebra.Basis.Submodule
Module.Basis.addSubgroupOfClosure_repr_apply : ∀ {M : Type u_7} {R : Type u_8} [inst : Ring R] [inst_1 : Nontrivial R] [inst_2 : IsAddTorsionFree R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (A : AddSubgroup M) {ι : Type u_9} (b : Module.Basis ι R M)
  (h : A = AddSubgroup.closure (Set.range ⇑b)) (x : ↥A) (i : ι),
  ↑(((Module.Basis.addSubgroupOfClosure A b h).repr x) i) = (b.repr ↑x) i
-- Mathlib.RingTheory.Coalgebra.Basic
DFinsupp.comul_comp_lsingle : ∀ (R : Type u) (ι : Type v) (A : ι → Type w) [inst : DecidableEq ι] [inst_1 : CommSemiring R]
  [inst_2 : (i : ι) → AddCommMonoid (A i)] [inst_3 : (i : ι) → Module R (A i)]
  [inst_4 : (i : ι) → CoalgebraStruct R (A i)] (i : ι),
  CoalgebraStruct.comul ∘ₗ DFinsupp.lsingle i =
    TensorProduct.map (DFinsupp.lsingle i) (DFinsupp.lsingle i) ∘ₗ CoalgebraStruct.comul