mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.id : {C : Type u} → (X : CategoryTheory.FreeMonoidalCategory C) → X.Hom X
-- Mathlib.Data.List.DropRight
List.mem_rtakeWhile_imp : ∀ {α : Type u_1} {p : α → Bool} {l : List α} {x : α}, x ∈ List.rtakeWhile p l → p x = true
-- Mathlib.Algebra.Algebra.Defs
RingHom.algebraMap_toAlgebra : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (i : R →+* S), algebraMap R S = i
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
/-- A `WeierstrassCurve` is in normal form of characteristic ≠ 2, if its `a₁, a₃ = 0`.
In other words it is `Y² = X³ + a₂X² + a₄X + a₆`.  -/
WeierstrassCurve.IsCharNeTwoNF : {R : Type u_1} → [CommRing R] → WeierstrassCurve R → Prop
-- Mathlib.Order.ULift
ULift.up_lt : ∀ {α : Type u} [inst : LT α] {a b : α}, { down := a } < { down := b } ↔ a < b
-- Mathlib.Logic.Nontrivial.Defs
not_subsingleton : ∀ (α : Type u_3) [Nontrivial α], ¬Subsingleton α
-- Mathlib.Algebra.Group.Hom.Defs
/-- Additive group homomorphisms preserve subtraction.  -/
map_add_neg : ∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddGroup G]
  [inst_2 : SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (a b : G), f (a + -b) = f a + -f b
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k fallback : α},
  k ∉ m → l.contains k = false → (m.insertManyIfNewUnit l).getKeyD k fallback = fallback
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.det_inv : ∀ {M : Type u_2} [inst : AddCommGroup M] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {A : Type u_5}
  [inst_3 : CommRing A] [inst_4 : Module A M] (b b' : Module.Basis ι A M), ↑⋯.unit⁻¹ = b'.det ⇑b
-- Mathlib.Tactic.Linarith.Preprocessing
/-- `nlinarithExtras` is the preprocessor corresponding to the `nlinarith` tactic.

* For every term `t` such that `t^2` or `t*t` appears in the input, adds a proof of `t^2 ≥ 0`
  or `t*t ≥ 0`.
* For every pair of comparisons `t1 R1 0` and `t2 R2 0`, adds a proof of `t1*t2 R 0`.

This preprocessor is typically run last, after all inputs have been canonized.
 -/
Mathlib.Tactic.Linarith.nlinarithExtras : Mathlib.Tactic.Linarith.GlobalPreprocessor
-- Mathlib.Topology.Algebra.Ring.Basic
instContinuousNegMulOpposite : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : TopologicalSpace R] [ContinuousNeg R], ContinuousNeg Rᵐᵒᵖ
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.isCaratheodory_empty : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α), m.IsCaratheodory ∅
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMk₄_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 4}
  (app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝) (app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝)
  (app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝) (app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝)
  (app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝)
  (w₀ :
    CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝)
        app₁.hom =
      CategoryTheory.CategoryStruct.comp app₀.hom
        (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝))
  (w₁ :
    CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_363✝) app₂.hom =
      CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_246✝ _proof_363✝))
  (w₂ :
    CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_364✝) app₃.hom =
      CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_299✝ _proof_364✝))
  (w₃ :
    CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_365✝) app₄.hom =
      CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 _proof_364✝ _proof_365✝)),
  (CategoryTheory.ComposableArrows.isoMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).inv =
    CategoryTheory.ComposableArrows.homMk₄ app₀.inv app₁.inv app₂.inv app₃.inv app₄.inv ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.Num.Prime
_private.Mathlib.Data.Num.Prime.0.PosNum.minFacAux.match_1.eq_1 : ∀ (motive : ℕ → PosNum → Sort u_1) (x : PosNum) (h_1 : (x : PosNum) → motive 0 x)
  (h_2 : (fuel : ℕ) → (k : PosNum) → motive fuel.succ k),
  (match 0, x with
    | 0, x => h_1 x
    | fuel.succ, k => h_2 fuel k) =
    h_1 x
-- Mathlib.Algebra.Group.Submonoid.Pointwise
coe_mul_coe : ∀ {M : Type u_3} {S : Type u_6} [inst : Monoid M] [inst_1 : SetLike S M] [SubmonoidClass S M] (H : S), ↑H * ↑H = ↑H
-- Mathlib.Data.Multiset.AddSub
Multiset.zero_add : ∀ {α : Type u_1} (s : Multiset α), 0 + s = s
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.leastGE.eq_1 : ∀ {ι : Type u_1} {Ω : Type u_2} {β : Type u_3} [inst : Preorder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι]
  [inst_3 : Preorder β] (f : ι → Ω → β) (r : β), MeasureTheory.leastGE f r = MeasureTheory.hittingAfter f (Set.Ici r) ⊥
-- Mathlib.FieldTheory.KummerExtension
finrank_of_isSplittingField_X_pow_sub_C : ∀ {K : Type u} [inst : Field K] {n : ℕ},
  (primitiveRoots n K).Nonempty →
    ∀ {a : K},
      Irreducible (Polynomial.X ^ n - Polynomial.C a) →
        ∀ (L : Type u_1) [inst_1 : Field L] [inst_2 : Algebra K L]
          [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)], Module.finrank K L = n
-- Init.Data.UInt.Lemmas
USize.toBitVec_ofNatLT : ∀ {n : ℕ} (hn : n < USize.size), (USize.ofNatLT n hn).toBitVec = n#'hn
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_eq_norm_of_mul_conj : ∀ {K : Type u_1} [inst : RCLike K] (x : K), RCLike.re (x * (starRingEnd K) x) = ‖x * (starRingEnd K) x‖
-- Init.Data.List.Attach
_private.Init.Data.List.Attach.0.List.findSome?.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.isPullback_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  sq.IsPullback ↔ Nonempty (CategoryTheory.Limits.IsLimit sq.pullbackCone)
-- Aesop.Percent
Aesop.Percent.instMul : Mul Aesop.Percent
-- Init.Data.UInt.Lemmas
UInt64.toNat.eq_1 : ∀ (n : UInt64), n.toNat = n.toBitVec.toNat
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.map_of : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : α), (FreeMonoid.map f) (FreeMonoid.of x) = FreeMonoid.of (f x)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.lcm_eq_inf : ∀ {A : Type u_2} [inst : CommRing A] [inst_1 : IsDedekindDomain A] (I J : Ideal A), lcm I J = I ⊓ J
-- Init.Grind.Ring.Field
/-- The inverse of a non-zero element is a right inverse.  -/
Lean.Grind.Field.mul_inv_cancel : ∀ {α : Type u} [self : Lean.Grind.Field α] {a : α}, a ≠ 0 → a * a⁻¹ = 1
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_counitIso_inv_app_right : ∀ {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] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₂ R),
  ((CategoryTheory.Comma.mapLeftIso R i).counitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.MeasureTheory.Measure.Restrict
piecewise_ae_eq_restrict : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → β}
  [inst_1 : DecidablePred fun x => x ∈ s], MeasurableSet s → s.piecewise f g =ᵐ[μ.restrict s] f
-- Init.Data.Nat.MinMax
Nat.min_zero : ∀ (a : ℕ), min a 0 = 0
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.map_comp_forget : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G),
  (CategoryTheory.Pseudofunctor.Grothendieck.map α).comp (CategoryTheory.Pseudofunctor.Grothendieck.forget G) =
    CategoryTheory.Pseudofunctor.Grothendieck.forget F
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.domDomCongrEquiv_apply : ∀ {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] [inst_5 : TopologicalSpace M₂]
  [inst_6 : TopologicalSpace M₃] {ι' : Type u_1} (e : ι ≃ ι') (f : ContinuousMultilinearMap R (fun x => M₂) M₃),
  (ContinuousMultilinearMap.domDomCongrEquiv e) f = ContinuousMultilinearMap.domDomCongr e f
-- Init.Data.String.Basic
String.Pos.ofSliceTo_startPos : ∀ {s : String} {pos : s.Pos}, String.Pos.ofSliceTo (s.sliceTo pos).startPos = s.startPos
-- Mathlib.Algebra.FiveLemma
/-- A special case of the five lemma in terms of modules. For a diagram explaining the variables,
see the module docstring.  -/
LinearMap.bijective_of_surjective_of_bijective_of_right_exact : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_7} {N₂ : Type u_8}
  {N₃ : Type u_9} [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃]
  [inst_4 : Module R M₁] [inst_5 : Module R M₂] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁]
  [inst_8 : AddCommGroup N₂] [inst_9 : AddCommGroup N₃] [inst_10 : Module R N₁] [inst_11 : Module R N₂]
  [inst_12 : Module R N₃] (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (i₁ : M₁ →ₗ[R] N₁)
  (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃),
  g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁ →
    g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂ →
      Function.Exact ⇑f₁ ⇑f₂ →
        Function.Exact ⇑g₁ ⇑g₂ →
          Function.Surjective ⇑i₁ →
            Function.Bijective ⇑i₂ → Function.Surjective ⇑f₂ → Function.Surjective ⇑g₂ → Function.Bijective ⇑i₃
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.perm_mapsTo_inl_iff_mapsTo_inr : ∀ {m : Type u_1} {n : Type u_2} [Finite m] [Finite n] (σ : Equiv.Perm (m ⊕ n)),
  Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.instSMulCommClassSubtypeMem_1 : ∀ {M' : Type u_1} {α : Type u_2} {β : Type u_3} {S' : Type u_4} [inst : SetLike S' M'] (s : S') [inst_1 : SMul α β]
  [inst_2 : SMul M' β] [SMulCommClass α M' β], SMulCommClass α (↥s) β
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.brecOn : ∀ {R : Type u} {X : Type v} [inst : CommRing R]
  {motive : (a a_1 : FreeNonUnitalNonAssocAlgebra R X) → FreeLieAlgebra.Rel R X a a_1 → Prop}
  {a a_1 : FreeNonUnitalNonAssocAlgebra R X} (t : FreeLieAlgebra.Rel R X a a_1),
  (∀ (a a_2 : FreeNonUnitalNonAssocAlgebra R X) (t : FreeLieAlgebra.Rel R X a a_2),
      FreeLieAlgebra.Rel.below t → motive a a_2 t) →
    motive a a_1 t
-- Plausible.Gen
/-- Print (at most) 10 samples of a given type to stdout for debugging. Sadly specialized to `Type 0`
 -/
Plausible.Gen.printSamples : {t : Type} → [Repr t] → Plausible.Gen t → IO PUnit.{1}
-- Mathlib.Analysis.Complex.Exponential
Real.exp_strictMono : StrictMono Real.exp
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.isNormal_comap : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) {S : CategoryTheory.Subgroupoid D},
  S.IsNormal → (CategoryTheory.Subgroupoid.comap φ S).IsNormal
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
IsIntegral.of_finite : ∀ (R : Type u_1) {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] [Module.Finite R B]
  (x : B), IsIntegral R x
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteBooleanAlgebra.toCompleteDistribLattice : {α : Type u} → [CompleteBooleanAlgebra α] → CompleteDistribLattice α
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.π_descH_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : h.K ⟶ A)
  (hk : CategoryTheory.CategoryStruct.comp h.f' k = 0) {Z : C} (h_1 : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.π (CategoryTheory.CategoryStruct.comp (h.descH k hk) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
_private.Mathlib.Combinatorics.SimpleGraph.Triangle.Counting.0.SimpleGraph.edgeDensity_badVertices_le : ∀ {α : Type u_1} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {ε : ℝ} {s t : Finset α},
  0 ≤ ε →
    2 * ε ≤ ↑(G.edgeDensity s t) → ↑(G.edgeDensity (SimpleGraph.badVertices✝ G ε s t) t) ≤ ↑(G.edgeDensity s t) - ε
-- Mathlib.Geometry.Euclidean.Inversion.Calculus
ContDiffWithinAt.inversion : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : InnerProductSpace ℝ F] {c x : E → F} {R : E → ℝ} {s : Set E} {a : E} {n : ℕ∞},
  ContDiffWithinAt ℝ (↑n) c s a →
    ContDiffWithinAt ℝ (↑n) R s a →
      ContDiffWithinAt ℝ (↑n) x s a →
        x a ≠ c a → ContDiffWithinAt ℝ (↑n) (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) s a
-- Mathlib.Algebra.Ring.Equiv
/-- Product of a singleton family of (non-unital non-associative semi)rings is isomorphic
to the only member of this family.  -/
RingEquiv.piUnique : {ι : Type u_7} →
  (R : ι → Type u_8) →
    [inst : Unique ι] → [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (R i)] → ((i : ι) → R i) ≃+* R default
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- `leftSection` splits `g`  -/
CategoryTheory.IsSplitCoequalizer.leftSection_bottom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z}
  (self : CategoryTheory.IsSplitCoequalizer f g π),
  CategoryTheory.CategoryStruct.comp self.leftSection g = CategoryTheory.CategoryStruct.id Y
-- Std.Http.Data.URI.Encoding
/-- Creates an encoded query parameter from raw bytes, panicking on invalid encoding.
 -/
Std.Http.URI.EncodedQueryParam.ofByteArray! : ByteArray → Std.Http.URI.EncodedQueryParam
-- Mathlib.Algebra.Homology.Square
/-- The kernel fork attached to a commutative square in a preadditive category.  -/
CategoryTheory.Square.kernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (sq : CategoryTheory.Square C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct sq.X₂ sq.X₃] →
          CategoryTheory.Limits.KernelFork (CategoryTheory.Limits.biprod.desc sq.f₂₄ (-sq.f₃₄))
-- Init.Data.Nat.Basic
/-- Returns the lesser of two natural numbers. Usually accessed via `Min.min`.

Returns `n` if `n ≤ m`, or `m` if `m ≤ n`.

Examples:
* `min 0 5 = 0`
* `min 4 5 = 4`
* `min 4 3 = 3`
* `min 8 8 = 8`
 -/
Nat.min : ℕ → ℕ → ℕ
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Pos.Raw.extract.go₁.match_1.splitter : (motive : List Char → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw → Sort u_1) →
  (x : List Char) →
    (x_1 x_2 x_3 : String.Pos.Raw) →
      ((x x_4 x_5 : String.Pos.Raw) → motive [] x x_4 x_5) →
        ((c : Char) → (cs : List Char) → (i b e : String.Pos.Raw) → motive (c :: cs) i b e) → motive x x_1 x_2 x_3
-- Lean.Parser.Command
Lean.Parser.Command.extends.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Finset.NoncommProd
/-- The non-commutative version of `Finset.prod_mul_distrib`  -/
Finset.noncommProd_mul_distrib : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] {s : Finset α} (f g : α → β)
  (comm_ff : (↑s).Pairwise (Function.onFun Commute f)) (comm_gg : (↑s).Pairwise (Function.onFun Commute g))
  (comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)),
  s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
-- Mathlib.Algebra.ContinuedFractions.Translations
_private.Mathlib.Algebra.ContinuedFractions.Translations.0.GenContFract.contsAux.match_3.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((n : ℕ) → motive n.succ.succ) → motive x
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.uniqueGalZero : {F : Type u_1} → [inst : Field F] → Unique (Polynomial.Gal 0)
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Producer.mk.inj : ∀ {chunk : Std.Http.Chunk} {done : IO.Promise Bool} {chunk_1 : Std.Http.Chunk} {done_1 : IO.Promise Bool},
  { chunk := chunk, done := done } = { chunk := chunk_1, done := done_1 } → chunk = chunk_1 ∧ done = done_1
-- Lean.Environment
/-- The async branch that finished adding a declaration, i.e. `AddConstAsyncResult.asyncEnv`.  -/
Lean.AsyncBranch.asyncEnv : Lean.AsyncBranch
-- Mathlib.Algebra.Regular.Opposite
/-- **Alias** of the reverse direction of `isRightRegular_unop`. -/
IsRightRegular.unop : ∀ {R : Type u_1} [inst : Mul R] {a : Rᵐᵒᵖ}, IsLeftRegular a → IsRightRegular (MulOpposite.unop a)
-- Lean.Util.Path
Lean.getLibDir : System.FilePath → IO System.FilePath
-- Mathlib.RingTheory.Norm.Defs
Algebra.norm_natCast : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [Module.Free R S] (n : ℕ),
  (Algebra.norm R) ↑n = ↑n ^ Module.finrank R S
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_1 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w a : ℕ)
  (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, Std.Tactic.BVDecide.BVExpr.var a with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_1 w a
-- Mathlib.Order.Antisymmetrization
instTransLtAntisymmRelLe : {α : Type u_1} →
  [inst : Preorder α] → Trans (fun x1 x2 => x1 < x2) (AntisymmRel fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 < x2
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.mkPatternRefMap.go : Lean.Expr → (σ : Type) → ST σ (Lean.ExprMap Lean.Expr)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.symm_apply_eq : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (e : A ≃⋆ₐ[R] B) {x : B} {y : A},
  e.symm x = y ↔ x = e y
-- Mathlib.Order.Nucleus
Nucleus.toInfHom : {X : Type u_2} → [inst : SemilatticeInf X] → Nucleus X → InfHom X X
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.bot_prod_bot : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M], ⊥.prod ⊥ = ⊥
-- Mathlib.Analysis.Normed.Ring.Basic
nnnorm_commutator_units_sub_one_le : ∀ {α : Type u_2} [inst : SeminormedRing α] (a b : αˣ),
  ‖↑(a * b * a⁻¹ * b⁻¹) - 1‖₊ ≤ 2 * ‖↑a⁻¹‖₊ * ‖↑b⁻¹‖₊ * ‖↑a - 1‖₊ * ‖↑b - 1‖₊
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instZeroHom.eq_1 : ∀ (G H : AddCommGrpCat), G.instZeroHom H = { zero := AddCommGrpCat.ofHom 0 }
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
MeasureTheory.MeasurePreserving.aestronglyMeasurable_comp_iff : ∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace γ] {β : Type u_4} {f : α → β} {mα : MeasurableSpace α}
  {μa : MeasureTheory.Measure α} {mβ : MeasurableSpace β} {μb : MeasureTheory.Measure β},
  MeasureTheory.MeasurePreserving f μa μb →
    MeasurableEmbedding f →
      ∀ {g : β → γ}, MeasureTheory.AEStronglyMeasurable (g ∘ f) μa ↔ MeasureTheory.AEStronglyMeasurable g μb
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.GrothendieckTopology C}
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  (F : CategoryTheory.Sheaf J A) {X Y Z : C} (f : G.obj X ⟶ G.obj Y) (g : G.obj Y ⟶ G.obj Z) {Z_1 : A}
  (h : F.obj.obj (Opposite.op X) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F f) h)
-- Mathlib.GroupTheory.Sylow
/-- Auxiliary lemma for `Sylow.not_dvd_index` which is strictly stronger.  -/
_private.Mathlib.GroupTheory.Sylow.0.Sylow.not_dvd_index_aux : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [hp : Fact (Nat.Prime p)] (P : Sylow p G) [(↑P).Normal] [(↑P).FiniteIndex],
  ¬p ∣ (↑P).index
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₃_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y),
  CategoryTheory.ShortComplex.SnakeInput.functorL₃.map f = f.f₃
-- Mathlib.RingTheory.DividedPowers.DPMorphism
/-- Given divided power structures on the `A`-ideal `I` and the `B`-ideal `J`, a ring morphism
`A → B` is a divided power morphism if it is compatible with these divided power structures.  -/
DividedPowers.IsDPMorphism : {A : Type u_1} →
  {B : Type u_2} →
    [inst : CommSemiring A] →
      [inst_1 : CommSemiring B] → {I : Ideal A} → {J : Ideal B} → DividedPowers I → DividedPowers J → (A →+* B) → Prop
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y),
  (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₁ = f.f₀.τ₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyGT?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getKeyGT? k = t₂.getKeyGT? k