mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.mk.congr_simp : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} (toWord toWord_1 : Monoid.CoprodI.Word G)
  (e_toWord : toWord = toWord_1) (head head_1 : H),
  head = head_1 →
    ∀ (normalized : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ toWord.toList → g ∈ d.set i),
      { toWord := toWord, head := head, normalized := normalized } =
        { toWord := toWord_1, head := head_1, normalized := ⋯ }
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.map_neg : ∀ {α β : Type u} (f : α → β) (x : FreeAddGroup α), f <$> (-x) = -f <$> x
-- Mathlib.CategoryTheory.Sites.Equivalence
/-- Transport to a small model and sheafify there.  -/
CategoryTheory.smallSheafify : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₃) →
        [inst_1 : CategoryTheory.Category.{v₃, u₃} A] →
          [inst_2 : CategoryTheory.EssentiallySmall.{w, v₁, u₁} C] →
            [CategoryTheory.HasSheafify ((CategoryTheory.equivSmallModel C).inverse.inducedTopology J) A] →
              CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- If an element `a` divides another element `c` in a ring, `a` divides the sum of another element
`b` with `c` iff `a` divides `b`.  -/
dvd_add_left : ∀ {α : Type u_1} [inst : NonUnitalRing α] {a b c : α}, a ∣ c → (a ∣ b + c ↔ a ∣ b)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.opEquiv_counitIso : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T),
  (CategoryTheory.Comma.opEquiv L R).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.Iso.refl
          (((CategoryTheory.Comma.unopFunctor R L).leftOp.comp (CategoryTheory.Comma.opFunctor L R)).obj X))
      ⋯
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.AuxGluingStruct.metric : {A : Type} → [inst : MetricSpace A] → (self : GromovHausdorff.AuxGluingStruct A) → MetricSpace self.Space
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivial.symmₗ_trivialization : ∀ (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace B] (x : B),
  Bundle.Trivialization.symmₗ 𝕜 (Bundle.Trivial.trivialization B F) x = LinearMap.id
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.comp.match_1.splitter : {C : Type u_1} →
  (motive : CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → Sort u_2) →
    (x x_1 x_2 : CategoryTheory.WithInitial C) →
      ((_X _Y _Z : C) →
          motive (CategoryTheory.WithInitial.of _X) (CategoryTheory.WithInitial.of _Y)
            (CategoryTheory.WithInitial.of _Z)) →
        ((x : CategoryTheory.WithInitial C) →
            (_X : C) → motive CategoryTheory.WithInitial.star x (CategoryTheory.WithInitial.of _X)) →
          ((x : CategoryTheory.WithInitial C) →
              (_X : C) → motive x (CategoryTheory.WithInitial.of _X) CategoryTheory.WithInitial.star) →
            ((_Y : C) →
                (x : CategoryTheory.WithInitial C) →
                  motive (CategoryTheory.WithInitial.of _Y) CategoryTheory.WithInitial.star x) →
              (Unit →
                  motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star
                    CategoryTheory.WithInitial.star) →
                motive x x_1 x_2
-- Lean.Elab.Util
_private.Lean.Elab.Util.0.Lean.Elab.evalSyntaxConstantUnsafe : Lean.Environment → Lean.Options → Lean.Name → ExceptT String Id Lean.Syntax
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
Module.finrank_of_infinite_dimensional : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  ¬FiniteDimensional K V → Module.finrank K V = 0
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.digits.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (b : ℕ) → motive b.succ.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | b.succ.succ => h_3 b) =
    h_1 ()
-- Mathlib.Algebra.Order.Ring.Archimedean
/-- `ArchimedeanClass.mk` defines an `AddValuation` on the ring `R`.  -/
ArchimedeanClass.addValuation : (R : Type u_1) →
  [inst : LinearOrder R] →
    [inst_1 : CommRing R] → [inst_2 : IsStrictOrderedRing R] → AddValuation R (ArchimedeanClass R)
-- Aesop.Index.RulePattern
Aesop.RulePatternIndex.mk.inj : ∀ {tree : Lean.Meta.DiscrTree Aesop.RulePatternIndex.Entry} {isEmpty : Bool}
  {tree_1 : Lean.Meta.DiscrTree Aesop.RulePatternIndex.Entry} {isEmpty_1 : Bool},
  { tree := tree, isEmpty := isEmpty } = { tree := tree_1, isEmpty := isEmpty_1 } → tree = tree_1 ∧ isEmpty = isEmpty_1
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.mk : {I₁ : Type u_7} →
  {I₂ : Type u_8} →
    {I₃ : Type u_9} →
      {J : Type u_10} →
        {r : I₁ × I₂ × I₃ → J} →
          (I₂₃ : Type u_11) →
            (p : I₂ × I₃ → I₂₃) →
              (q : I₁ × I₂₃ → J) →
                (∀ (i : I₁ × I₂ × I₃), q (i.1, p i.2) = r i) → CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.coe_mkHomeomorph_symm : ∀ {M : Type u_1} [inst : TopologicalSpace M], ⇑DomMulAct.mkHomeomorph.symm = ⇑DomMulAct.mk.symm
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_nullSingletonClass' : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [h : Nonempty ι]
  [∀ (i : ι), MeasureTheory.NullSingletonClass (μ i)], MeasureTheory.NullSingletonClass (MeasureTheory.Measure.pi μ)
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal.eq_1 : ∀ (a : ENNReal), a.toReal = ↑a.toNNReal
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.nsmul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s : Finset α}, s.Nonempty → ∀ {n : ℕ}, (n • s).Nonempty
-- Mathlib.Order.Heyting.Basic
BiheytingAlgebra.toHeytingAlgebra : {α : Type u_4} → [self : BiheytingAlgebra α] → HeytingAlgebra α
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.toParserDescr.validAtom : Lean.Syntax → Lean.Elab.Term.ToParserDescrM String
-- Mathlib.Topology.Category.CompHaus.EffectiveEpi
CompHaus.effectiveEpi_tfae : ∀ {B X : CompHaus} (π : X ⟶ B),
  [CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π,
      Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)].TFAE
-- Std.Time.Date.Unit.Day
/-- Convert `Day.Offset` into `Millisecond.Offset`.
 -/
Std.Time.Day.Offset.toMilliseconds : Std.Time.Day.Offset → Std.Time.Millisecond.Offset
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.num_one : ∀ (z : UpperHalfPlane), UpperHalfPlane.num 1 ↑z = ↑z
-- Std.Sync.Mutex
/-- `mutex.tryAtomically k` tries to lock `mutex` and runs `k` on it if it succeeds. On success the
return value of `k` is returned as `some`, on failure `none` is returned.

This function does not block on the `mutex`. Additionally calling `mutex.tryAtomically` while
already holding the underlying `BaseMutex` in the same thread is undefined behavior. If this is
unavoidable in your code, consider using `RecursiveMutex`.
 -/
Std.Mutex.tryAtomically : {m : Type → Type} →
  {α β : Type} → [Monad m] → [MonadLiftT BaseIO m] → [MonadFinally m] → Std.Mutex α → Std.AtomicT α m β → m (Option β)
-- Mathlib.Geometry.Convex.Cone.TensorProduct
/-- The maximal tensor product of two cones is the dual (pointed cone) of the minimal tensor product
of the dual cones.  -/
PointedCone.maxTensorProduct : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : LinearOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {G : Type u_2} →
          [inst_3 : AddCommGroup G] →
            [inst_4 : Module R G] →
              {H : Type u_3} →
                [inst_5 : AddCommGroup H] →
                  [inst_6 : Module R H] → PointedCone R G → PointedCone R H → PointedCone R (TensorProduct R G H)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sSameSide_point_incenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SSameSide (s.points i) s.incenter
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instContinuousInv : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Inv G] [inst_2 : ContinuousInv G],
  ContinuousInv (SeparationQuotient G)
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.Num.gcdAux.match_1.splitter : (motive : ℕ → Num → Num → Sort u_1) →
  (x : ℕ) →
    (x_1 x_2 : Num) →
      ((x b : Num) → motive 0 x b) →
        ((n : ℕ) → (b : Num) → motive n.succ Num.zero b) →
          ((n : ℕ) → (a b : Num) → (a = Num.zero → False) → motive n.succ a b) → motive x x_1 x_2
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry_pre_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A B : C}
  [inst_2 : CategoryTheory.Closed A] [inst_3 : CategoryTheory.Closed B] (f : B ⟶ A) {X Y : C}
  (g : CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ X),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry g)
      ((CategoryTheory.MonoidalClosed.pre f).app X) =
    CategoryTheory.MonoidalClosed.curry
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) g)
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.exists_seq_antitone_tendsto_atTop_atBot : ∀ (α : Type u_3) [inst : Preorder α] [Nonempty α] [IsCodirectedOrder α] [Filter.atBot.IsCountablyGenerated],
  ∃ xs, Antitone xs ∧ Filter.Tendsto xs Filter.atTop Filter.atBot
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped
with Haar measure. Then the Lebesgue integral of the pointwise expression
`|u x| ^ (n / (n - 1))` is bounded above by a constant times the `n / (n - 1)`-th power of the
Lebesgue integral of the Fréchet derivative of `u`.  -/
MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {E : Type u_4} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : FiniteDimensional ℝ E]
  (μ : MeasureTheory.Measure E) [inst_7 : μ.IsAddHaarMeasure] {u : E → F},
  ContDiff ℝ 1 u →
    HasCompactSupport u →
      ∀ {p : ℝ},
        (↑(Module.finrank ℝ E)).HolderConjugate p →
          ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤
            ↑(MeasureTheory.lintegralPowLePowLIntegralFDerivConst μ p) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ p
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.GeometricallyConnected.geometrically_connectedSpace : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.GeometricallyConnected f],
  AlgebraicGeometry.geometrically (fun x => ConnectedSpace ↥x) f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.leanSorryLike.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.leanSorryLike = 1
-- Mathlib.Data.Finmap
Finmap.mem_singleton : ∀ {α : Type u} {β : α → Type v} (x y : α) (b : β y), x ∈ Finmap.singleton y b ↔ x = y
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instMin : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → Min (FractionalIdeal S P)
-- Mathlib.Algebra.Ring.InjSurj
/-- A type endowed with `-` and `*` has distributive negation, if it admits an injective map that
preserves `-` and `*` to a type which has distributive negation.  -/
Function.Injective.hasDistribNeg : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Mul S] →
      [inst_1 : Neg S] →
        (f : S → R) →
          Function.Injective f →
            [inst_2 : Mul R] →
              [inst_3 : HasDistribNeg R] →
                (∀ (a : S), f (-a) = -f a) → (∀ (a b : S), f (a * b) = f a * f b) → HasDistribNeg S
-- Mathlib.Algebra.MonoidAlgebra.Opposite
MonoidAlgebra.opRingEquiv_single : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : Mul M] (r : R) (x : M),
  MonoidAlgebra.opRingEquiv (MulOpposite.op (MonoidAlgebra.single x r)) =
    MonoidAlgebra.single (MulOpposite.op x) (MulOpposite.op r)
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Submodule.IsPrincipal.contentIdeal_eq_span_content_of_isPrincipal : ∀ {R : Type u_3} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p : Polynomial R},
  Submodule.IsPrincipal p.contentIdeal → p.contentIdeal = Ideal.span {p.content}
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.pushColumn : Lean.Parser.ParserFn
-- Init.Data.String.Lemmas.Order
String.Pos.lt_ofSlice_iff : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos},
  q < String.Pos.ofSlice p ↔ ∃ (h₁ : q ≤ p₁), ∀ (h₀ : p₀ ≤ q), q.slice p₀ p₁ h₀ h₁ < p
-- Mathlib.Algebra.GroupWithZero.Center
Set.center_units_subset : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀], Set.center G₀ˣ ⊆ Units.val ⁻¹' Set.center G₀
-- Mathlib.GroupTheory.Sylow
/-- A special case of **Sylow's first theorem**. If `G` is a `p`-group and `H` a subgroup of size at
least `p ^ n` then there is a subgroup of `H` of cardinality `p ^ n`.  -/
Sylow.exists_subgroup_le_card_pow_prime_of_le_card : ∀ {G : Type u} [inst : Group G] {n p : ℕ},
  Nat.Prime p → IsPGroup p G → ∀ {H : Subgroup G}, p ^ n ≤ Nat.card ↥H → ∃ H' ≤ H, Nat.card ↥H' = p ^ n
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.eval.eq_3 : ∀ (ns : List ℕ) (k : Turing.ToPartrec.Cont), (Turing.ToPartrec.Cont.cons₂ ns k).eval = fun v => k.eval (ns.headI :: v)
-- Init.Tactics
/-- `try tac` runs `tac` and succeeds even if `tac` failed.  -/
Lean.Parser.Tactic.tacticTry_ : Lean.ParserDescr
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β] {f g : α ≃+*o β}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WOppSide.trans_wSameSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, s.WOppSide x y → s.WSameSide y z → y ∉ s → s.WOppSide x z
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- The embedding of `C` into `Mat_ C` as one-by-one matrices.
(We index the summands by `PUnit`.)  -/
CategoryTheory.Mat_.embedding : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CategoryTheory.Functor C (CategoryTheory.Mat_ C)
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The canonical morphism `∐ functorObjTgtFamily f πX ⟶ ∐ functorObjTgtFamily f πY`
induced by a morphism `Arrow.mk πX ⟶ Arrow.mk πY`.  -/
CategoryTheory.SmallObject.functorMapTgt : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S T X Y : C} →
            {πX : X ⟶ S} →
              {πY : Y ⟶ T} →
                (CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY) →
                  [inst_1 :
                      CategoryTheory.Limits.HasColimitsOfShape
                        (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
                    [inst_2 :
                        CategoryTheory.Limits.HasColimitsOfShape
                          (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C] →
                      ∐ CategoryTheory.SmallObject.functorObjTgtFamily f πX ⟶
                        ∐ CategoryTheory.SmallObject.functorObjTgtFamily f πY
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)),
  (F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).inv.toNatTrans.app X =
    (F.map f).toFunctor.map ((F.mapId b₀).hom.toNatTrans.app X)
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.beq.match_1.eq_4 : ∀ {α : Type u_1} {β : Type u_2} (motive : Batteries.AssocList α β → Batteries.AssocList α β → Sort u_3) (a : α) (b : β)
  (t : Batteries.AssocList α β) (a' : α) (b' : β) (t' : Batteries.AssocList α β)
  (h_1 : Unit → motive Batteries.AssocList.nil Batteries.AssocList.nil)
  (h_2 :
    (key : α) →
      (value : β) →
        (tail : Batteries.AssocList α β) → motive (Batteries.AssocList.cons key value tail) Batteries.AssocList.nil)
  (h_3 :
    (key : α) →
      (value : β) →
        (tail : Batteries.AssocList α β) → motive Batteries.AssocList.nil (Batteries.AssocList.cons key value tail))
  (h_4 :
    (a : α) →
      (b : β) →
        (t : Batteries.AssocList α β) →
          (a' : α) →
            (b' : β) →
              (t' : Batteries.AssocList α β) →
                motive (Batteries.AssocList.cons a b t) (Batteries.AssocList.cons a' b' t')),
  (match Batteries.AssocList.cons a b t, Batteries.AssocList.cons a' b' t' with
    | Batteries.AssocList.nil, Batteries.AssocList.nil => h_1 ()
    | Batteries.AssocList.cons key value tail, Batteries.AssocList.nil => h_2 key value tail
    | Batteries.AssocList.nil, Batteries.AssocList.cons key value tail => h_3 key value tail
    | Batteries.AssocList.cons a b t, Batteries.AssocList.cons a' b' t' => h_4 a b t a' b' t') =
    h_4 a b t a' b' t'
-- Std.Http.Server
/-- Triggers cancellation of all requests and the accept loop in the server. This function should be used
in conjunction with `waitShutdown` to properly coordinate the shutdown sequence.
 -/
Std.Http.Server.shutdown : Std.Http.Server → Std.Async.Async Unit
-- Mathlib.Combinatorics.Configuration
Configuration.Nondegenerate.exists_point : ∀ {P : Type u_1} {L : Type u_2} {inst : Membership P L} [self : Configuration.Nondegenerate P L] (l : L), ∃ p, p ∉ l
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Two equal natural transformations `R₁ ⟶ R₂` yield naturally isomorphic functors
`P.Comma L R₁ Q W ⥤ P.Comma L R₂ Q W`.  -/
CategoryTheory.MorphismProperty.Comma.mapRightEq : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            (L : CategoryTheory.Functor A T) →
              {P : CategoryTheory.MorphismProperty T} →
                {Q : CategoryTheory.MorphismProperty A} →
                  {W : CategoryTheory.MorphismProperty B} →
                    [inst_3 : Q.IsMultiplicative] →
                      [inst_4 : W.IsMultiplicative] →
                        {R₁ R₂ : CategoryTheory.Functor B T} →
                          [Q.RespectsIso] →
                            [W.RespectsIso] →
                              (r r' : R₁ ⟶ R₂) →
                                (h : r = r') →
                                  (hr :
                                      ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
                                        P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right))) →
                                    CategoryTheory.MorphismProperty.Comma.mapRight L r hr ≅
                                      CategoryTheory.MorphismProperty.Comma.mapRight L r' ⋯
-- Init.Data.Option.Lemmas
Option.not_lt_none : ∀ {α : Type u_1} [inst : LT α] {a : Option α}, ¬a < none
-- Lean.Message
Lean.instTypeNameMessageData : TypeName Lean.MessageData
-- Mathlib.Algebra.Group.Defs
Group.toCancelMonoid : {G : Type u_1} → [Group G] → CancelMonoid G
-- Mathlib.Logic.Relation
/-- **Alias** of `Relation.ReflTransGen.stdSymm`. -/
Relation.ReflTransGen.symmetric : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r], Std.Symm (Relation.ReflTransGen r)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.diagonalCover.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (𝒱 :
    (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) →
      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover),
  AlgebraicGeometry.Scheme.Pullback.diagonalCover f 𝒰 𝒱 =
    CategoryTheory.Precoverage.ZeroHypercover.bind (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i =>
      AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight (𝒱 i) (𝒱 i)
        (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i) (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i)
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- A conditionally complete lattice is a lattice in which
every nonempty subset which is bounded above has a supremum, and
every nonempty subset which is bounded below has an infimum.
Typical examples are real numbers or natural numbers.

To differentiate the statements from the corresponding statements in (unconditional)
complete lattices, we prefix `sInf` and `sSup` by a `c` everywhere. The same statements should
hold in both worlds, sometimes with additional assumptions of nonemptiness or
boundedness.  -/
ConditionallyCompleteLattice : Type u_5 → Type u_5
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.induction_on : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {p : SkewMonoidAlgebra k G → Prop} (f : SkewMonoidAlgebra k G),
  p 0 →
    (∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)) →
      (∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)) → p f
-- Mathlib.Util.Export
Lean.Export.instCoeLevelEntry : Coe Lean.Level Lean.Export.Entry
-- Mathlib.RingTheory.PowerSeries.Exp
PowerSeries.isUnit_exp : ∀ (A : Type u_4) [inst : Ring A] [inst_1 : Algebra ℚ A], IsUnit (PowerSeries.exp A)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.quot_mul : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (x y : CommRingCat.Colimits.Prequotient F),
  Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) (x.mul y) =
    (have this := Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) x;
      this) *
      have this := Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) y;
      this
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.mapPower_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β : Type}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] [inst_2 : CategoryTheory.Limits.HasProductsOfShape β C]
  (f : α → β) (a : α) {Z : CategoryTheory.Limits.FormalCoproduct C} (h : U ⟶ Z),
  CategoryTheory.CategoryStruct.comp (U.mapPower f) (CategoryTheory.CategoryStruct.comp (U.powerπ a) h) =
    CategoryTheory.CategoryStruct.comp (U.powerπ (f a)) h
-- Init.Data.SInt.Lemmas
Int8.toInt32_ofIntLE : ∀ {n : ℤ} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt),
  (Int8.ofIntLE n h₁ h₂).toInt32 = Int32.ofIntLE n ⋯ ⋯
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.checkNoImmediateColon.parenthesizer : Lean.PrettyPrinter.Parenthesizer