mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.SubarrayIterator.step_eq : ∀ {α : Type u_1} {it : Std.Iter α},
  it.step =
    if h : it.internalState.xs.start < it.internalState.xs.stop then
      ⟨Std.IterStep.yield
          {
            internalState :=
              {
                xs :=
                  {
                    internalRepresentation :=
                      { array := it.internalState.xs.array, start := it.internalState.xs.start + 1,
                        stop := it.internalState.xs.stop, start_le_stop := ⋯, stop_le_array_size := ⋯ } } } }
          it.internalState.xs.array[it.internalState.xs.start],
        ⋯⟩
    else ⟨Std.IterStep.done, ⋯⟩
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdLocallyUniformly.hasProdLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β], HasProdLocallyUniformly f g → HasProdLocallyUniformlyOn f g s
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation.ite : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {op₁ op₂ :
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation op₁ →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation op₂ →
      ∀ {P : Option (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl) → Prop} [inst : DecidablePred P],
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation fun ms =>
          if P ms.head then op₁ ms else op₂ ms
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev_eq_posLT : ∀ {s : String} {p : s.Pos} {h : p ≠ s.startPos}, p.prev h = s.posLT p.offset ⋯
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.coe_opensOfIdeal : ∀ {X : Type u_1} {R : Type u_2} [inst : TopologicalSpace X] [inst_1 : Semiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : T2Space R] (I : Ideal C(X, R)),
  ↑(ContinuousMap.opensOfIdeal I) = ContinuousMap.setOfIdeal I
-- Mathlib.InformationTheory.Hamming
Hamming.instDiscreteTopology : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)],
  DiscreteTopology (Hamming β)
-- Mathlib.Control.Bitraversable.Lemmas
/-- traverse on the first functor argument  -/
Bitraversable.tfst : {t : Type u → Type u → Type u} →
  [Bitraversable t] →
    {β : Type u} → {F : Type u → Type u} → [Applicative F] → {α α' : Type u} → (α → F α') → t α β → F (t α' β)
-- Mathlib.Algebra.Group.Defs
nsmulRec_add : ∀ {M : Type u} [inst : Zero M] [inst_1 : AddSemigroup M] (m n : ℕ),
  n ≠ 0 → ∀ (a : M), 0 + a = a → nsmulRec (m + n) a = nsmulRec m a + nsmulRec n a
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.MkTableKey.State.mk : ℕ →
  Std.HashMap Lean.LMVarId Lean.Level →
    Std.HashMap Lean.MVarId Lean.Expr → Lean.MetavarContext → Lean.Meta.SynthInstance.MkTableKey.State
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.dvd_of_mem_finMulAntidiag : ∀ {n d : ℕ} {f : Fin d → ℕ}, f ∈ d.finMulAntidiag n → ∀ (i : Fin d), f i ∣ n
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.lift_mk_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasImage g]
  [inst_2 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)]
  (h : Y ⟶ CategoryTheory.Limits.image g)
  (H :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.Limits.image.ι g) =
      CategoryTheory.CategoryStruct.comp f g)
  {Z_1 : C} (h_1 : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.image.lift
        { I := CategoryTheory.Limits.image g, m := CategoryTheory.Limits.image.ι g, m_mono := ⋯,
          e := CategoryTheory.CategoryStruct.comp f h, fac := ⋯ })
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι g) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) h_1
-- Init.Data.Vector.DecidableEq
Vector.eq_of_isEqv : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (xs ys : Vector α n),
  (xs.isEqv ys fun x y => decide (x = y)) = true → xs = ys
-- Init.Data.SInt.Basic
instReprInt64 : Repr Int64
-- Mathlib.LinearAlgebra.Prod
Submodule.range_snd : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], (LinearMap.snd R M M₂).range = ⊤
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.prod_ext_iff : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃]
  [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃]
  {f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)},
  f = g ↔
    (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap f =
        (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap g ∧
      (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap f =
        (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap g
-- Std.Data.ExtHashMap.Lemmas
_private.Std.Data.ExtHashMap.Lemmas.0.Std.ExtHashMap.ext_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m m' : Std.ExtHashMap α β}, m = m' ↔ m.inner = m'.inner
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.inv_eq_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [inst_1 : CategoryTheory.IsIso f]
  [inst_2 : CategoryTheory.IsIso g], CategoryTheory.inv f = CategoryTheory.inv g ↔ f = g
-- Mathlib.RingTheory.Jacobson.Ring
MvPolynomial.isJacobsonRing_MvPolynomial_fin : ∀ {R : Type u} [inst : CommRing R] [H : IsJacobsonRing R] (n : ℕ), IsJacobsonRing (MvPolynomial (Fin n) R)
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.isSolvable_iff : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.IsSolvable L ↔ ∃ k, LieAlgebra.derivedSeries R L k = ⊥
-- Mathlib.Order.Filter.AtTopBot.Archimedean
PNat.tendsto_comp_val_iff : ∀ {β : Type u_3} {f : ℕ → β} {l : Filter β},
  Filter.Tendsto (fun x => f ↑x) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabel : Type
-- Mathlib.CategoryTheory.GlueData
/-- (Implementation detail) the constructed `GlueData.t'` from a `GlueData'`.  -/
CategoryTheory.GlueData'.t'' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (D : CategoryTheory.GlueData' C) →
      (i j k : D.J) →
        CategoryTheory.Limits.pullback (D.f' i j) (D.f' i k) ⟶ CategoryTheory.Limits.pullback (D.f' j k) (D.f' j i)
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.subRight_apply : ∀ {G : Type u_5} [inst : AddGroup G] (a b : G), (Equiv.subRight a) b = b - a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_a₂ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (f : R →+* A),
  (W.map f).a₂ = f W.a₂
-- Init.Omega.Int
Lean.Omega.Int.sub_congr : ∀ {a b c d : ℤ}, a = b → c = d → a - c = b - d
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.Generators.H.injEq : ∀ {B : Type v} (a a_1 : B), (CartanMatrix.Generators.H a = CartanMatrix.Generators.H a_1) = (a = a_1)
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.isOpen_iff_isUpperSet : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpperSet α] {s : Set α},
  IsOpen s ↔ IsUpperSet s
-- Mathlib.CategoryTheory.Elements
/-- The equivalence between the category of elements `F.Elements`
and the comma category `(*, F)`.  -/
CategoryTheory.CategoryOfElements.structuredArrowEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C (Type w)) → F.Elements ≌ CategoryTheory.StructuredArrow PUnit.{w + 1} F
-- Mathlib.Topology.UniformSpace.UniformConvergence
tendstoUniformlyOn_iff_tendstoUniformly_comp_coe : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {p : Filter ι}, TendstoUniformlyOn F f p s ↔ TendstoUniformly (fun i x => F i ↑x) (f ∘ Subtype.val) p
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
/-- Reinterpret a graded algebra homomorphism as a graded ring homomorphism.  -/
GradedAlgHom.toGradedRingHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {ι : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : DecidableEq ι] →
                    [inst_6 : AddMonoid ι] →
                      {𝒜 : ι → Submodule R A} →
                        {ℬ : ι → Submodule R B} →
                          [inst_7 : GradedAlgebra 𝒜] → [inst_8 : GradedAlgebra ℬ] → (𝒜 →ₐᵍ[R] ℬ) → 𝒜 →+*ᵍ ℬ
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.denoteS.match_1.eq_4 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a b : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (v : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var v))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_6 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match a.add b with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.var v => h_3 v
    | a.add b => h_4 a b
    | a.mul b => h_5 a b
    | a.pow k => h_6 a k
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_4 a b
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.mul_lt_const_weak : ∀ {α : Type u_1} {b c : α} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α],
  b < c → ∀ {a : α}, 0 ≤ a → b * a ≤ c * a
-- Mathlib.Order.Atoms
OrderEmbedding.isCoatom_of_map_top_of_image : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderTop α]
  [inst_3 : OrderTop β] (f : β ↪o α), f ⊤ = ⊤ → ∀ {b : β}, IsCoatom (f b) → IsCoatom b
-- Lean.Data.Lsp.Internal
/-- Used in the `$/lean/importClosure` watchdog <- worker notification.
Contains the full import closure of the file managed by a worker.
 -/
Lean.Lsp.LeanImportClosureParams : Type
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivary_neg_left`. -/
Monovary.neg_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Monovary f g → Antivary (-f) g
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.getInst : Lean.Name → Lean.Level → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Init.Data.SInt.Basic
/-- Computes the absolute value of a 16-bit signed integer.

This function is equivalent to `if a < 0 then -a else a`, so in particular `Int16.minValue` will be
mapped to `Int16.minValue`.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.abs : Int16 → Int16
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.imp.inj : ∀ {a a_1 a_2 a_3 : Mathlib.Tactic.ITauto.IProp}, a.imp a_1 = a_2.imp a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Lift a ring homomorphism that maps polynomials `φ : R[X] →+* S[X]`
to a `R⟮X⟯ →+* S⟮X⟯`,
on the condition that `φ` maps non-zero-divisors to non-zero-divisors,
by mapping both the numerator and denominator and quotienting them.  -/
RatFunc.mapRingHom : {R : Type u_3} →
  {S : Type u_4} →
    {F : Type u_5} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : FunLike F (Polynomial R) (Polynomial S)] →
            [inst_3 : RingHomClass F (Polynomial R) (Polynomial S)] →
              (φ : F) →
                nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S)) →
                  RatFunc R →+* RatFunc S
-- Mathlib.Algebra.Order.GroupWithZero.Basic
StrictMono.mul : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] [inst_2 : Preorder α]
  {f g : α → M₀} [PosMulStrictMono M₀] [MulPosStrictMono M₀],
  StrictMono f → StrictMono g → (∀ (x : α), 0 ≤ f x) → (∀ (x : α), 0 ≤ g x) → StrictMono (f * g)
-- Init.Data.Fin.Lemmas
Fin.succ_mk : ∀ (n i : ℕ) (h : i < n), ⟨i, h⟩.succ = ⟨i + 1, ⋯⟩
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.liftEquiv_id : ∀ {K : Type u_1} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing M] (p : ℕ) [inst_2 : ExpChar M p]
  [inst_3 : ExpChar K p] [inst_4 : PerfectRing M p], PerfectRing.liftEquiv M (RingHom.id K) p = Equiv.refl (K →+* M)
-- Init.Data.String.Lemmas.Order
String.Pos.le_ofSliceTo_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos},
  q ≤ String.Pos.ofSliceTo p ↔ ∃ (h : q ≤ p₀), p₀.sliceTo q h ≤ p
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.comonadToFunctor_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C),
  (CategoryTheory.comonadToFunctor C).obj G = G.toFunctor
-- Lean.Meta.CongrTheorems
/-- It is not a parameter for the congruence theorem, the theorem was specialized for this parameter.
This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it.  -/
Lean.Meta.CongrArgKind.fixedNoParam : Lean.Meta.CongrArgKind
-- Init.Omega.Int
Lean.Omega.Int.ofNat_sub_eq_zero : ∀ {b a : ℕ}, ¬b ≤ a → ↑(a - b) = 0
-- Mathlib.CategoryTheory.Filtered.Final
CategoryTheory.IsFiltered.final_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsFiltered C], (CategoryTheory.Prod.snd C D).Final
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Hom.residueDegree_id : ∀ {X : AlgebraicGeometry.Scheme} (x : ↥X),
  AlgebraicGeometry.Scheme.Hom.residueDegree (CategoryTheory.CategoryStruct.id X) x = 1
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.productTriangle_mor₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T : J → CategoryTheory.Pretriangulated.Triangle C) [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁],
  (CategoryTheory.Pretriangulated.productTriangle T).mor₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map fun j => (T j).mor₃)
      (CategoryTheory.inv (CategoryTheory.Limits.piComparison (CategoryTheory.shiftFunctor C 1) fun j => (T j).obj₁))
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainBialgHom.eq_1 : ∀ (R : Type u_1) {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : Monoid M] [inst_2 : Monoid N]
  (f : M →* N), MonoidAlgebra.mapDomainBialgHom R f = BialgHom.ofAlgHom (MonoidAlgebra.mapDomainAlgHom R R f) ⋯ ⋯
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Variant of `lift` in the case when the domain of `f` lies in the image of `F.obj`. Thus,
in this case, one can obtain the lift directly by giving two morphisms in `C`.  -/
CategoryTheory.Functor.relativelyRepresentable.lift' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {Y : D} →
            {b : C} →
              {f' : F.obj b ⟶ Y} →
                (hf' : F.relativelyRepresentable f') →
                  {a : C} →
                    {g : F.obj a ⟶ Y} →
                      {c : C} →
                        (i : c ⟶ b) →
                          (h : c ⟶ a) →
                            CategoryTheory.CategoryStruct.comp (F.map i) f' =
                                CategoryTheory.CategoryStruct.comp (F.map h) g →
                              [F.Full] → c ⟶ hf'.pullback g
-- ProofWidgets.Compat
ProofWidgets.ExprWithCtx.mk.injEq : ∀ (ci : Lean.Elab.ContextInfo) (lctx : Lean.LocalContext) (linsts : Lean.LocalInstances) (expr : Lean.Expr)
  (ci_1 : Lean.Elab.ContextInfo) (lctx_1 : Lean.LocalContext) (linsts_1 : Lean.LocalInstances) (expr_1 : Lean.Expr),
  ({ ci := ci, lctx := lctx, linsts := linsts, expr := expr } =
      { ci := ci_1, lctx := lctx_1, linsts := linsts_1, expr := expr_1 }) =
    (ci = ci_1 ∧ lctx = lctx_1 ∧ linsts = linsts_1 ∧ expr = expr_1)
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.map_nhds_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  Filter.map φ.leftFun (nhds φ.pt) = nhds (φ.leftFun φ.pt)
-- Mathlib.Topology.Algebra.Group.Defs
/-- Basic hypothesis to talk about a topological group. A topological group over `M`, for example,
is obtained by requiring the instances `Group M` and `ContinuousMul M` and
`ContinuousInv M`.  -/
ContinuousInv : (G : Type u) → [TopologicalSpace G] → [Inv G] → Prop
-- Mathlib.Data.Set.Image
Set.range_eq_univ : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α}, Set.range f = Set.univ ↔ Function.Surjective f
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.embedding_injective : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : GroupWithZero B] {f : A →*₀ B},
  Function.Injective ⇑MonoidWithZeroHom.ValueGroup₀.embedding
-- Mathlib.Tactic.Sat.FromLRAT
/-- A macro for producing SAT proofs from CNF / LRAT files.
These files are commonly used in the SAT community for writing proofs.

The input to the `lrat_proof` command is the name of the theorem to define,
and the statement (written in CNF format) and the proof (in LRAT format).
For example:
```
lrat_proof foo
  "p cnf 2 4  1 2 0  -1 2 0  1 -2 0  -1 -2 0"
  "5 -2 0 4 3 0  5 d 3 4 0  6 1 0 5 1 0  6 d 1 0  7 0 5 2 6 0"
```
produces a theorem:
```
foo : ∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1
```

* You can see the theorem statement by hovering over the word `foo`.
* You can use the `example` keyword in place of `foo` to avoid generating a theorem.
* You can use the `include_str` macro in place of the two strings
  to load CNF / LRAT files from disk.
 -/
Mathlib.Tactic.Sat.commandLrat_proof_Example____ : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.Bounded
eventually_cobounded_le_norm' : ∀ {E : Type u_2} [inst : SeminormedGroup E] (a : ℝ), ∀ᶠ (x : E) in Bornology.cobounded E, a ≤ ‖x‖
-- Mathlib.Order.Sublattice
Sublattice.prod_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (L : Sublattice α), L.prod ⊥ = ⊥
-- Init.Data.Range.Polymorphic.Basic
Std.Rco.mem_iff : ∀ {α : Type u} {r : Std.Rco α} {a : α} [inst : LE α] [inst_1 : LT α], a ∈ r ↔ r.lower ≤ a ∧ a < r.upper
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.derivedSeries_le_lowerCentralSeries : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (k : ℕ),
  LieAlgebra.derivedSeries R L k ≤ LieModule.lowerCentralSeries R L L k
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- metric space instance on the product of finitely many metric spaces, using the `L^p` distance,
and having as uniformity the product uniformity.  -/
PiLp.instMetricSpace : (p : ENNReal) →
  {ι : Type u_2} →
    (α : ι → Type u_3) → [hp : Fact (1 ≤ p)] → [Fintype ι] → [(i : ι) → MetricSpace (α i)] → MetricSpace (PiLp p α)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} {fallback : β k},
  (List.map Sigma.fst l).contains k = false → (Std.DTreeMap.Raw.ofList l cmp).getD k fallback = fallback
-- Mathlib.Analysis.Distribution.TemperedDistribution
MeasureTheory.Lp.toTemperedDistribution_toLp_eq : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [inst_4 : CompleteSpace F] [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E]
  {μ : MeasureTheory.Measure E} [hμ : μ.HasTemperateGrowth] [inst_7 : SecondCountableTopology E] {p : ENNReal}
  [hp : Fact (1 ≤ p)] (f : SchwartzMap E F),
  MeasureTheory.Lp.toTemperedDistribution (f.toLp p μ) = (SchwartzMap.toTemperedDistributionCLM E F μ) f
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.πE_EIsoH_hom_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f₁ : i₀ ⟶ i₁) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.πE_EIsoH_hom._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.πE_EIsoH_hom._auto_3) {Z : C}
  (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (X.πE (CategoryTheory.CategoryStruct.id i₀) f₁ (CategoryTheory.CategoryStruct.id i₁) n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X.EIsoH f₁ n₀ n₁ n₂ hn₁ hn₂).hom h) =
    CategoryTheory.CategoryStruct.comp (X.cyclesIsoH f₁ n₁ n₂ hn₂).hom h
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.differentiableAt_cuspFunction_zero : ∀ {h : ℝ} {f : ℂ → ℂ},
  0 < h →
    Function.Periodic f ↑h →
      (∀ᶠ (z : ℂ) in Filter.comap Complex.im Filter.atTop, DifferentiableAt ℂ f z) →
        (Filter.comap Complex.im Filter.atTop).BoundedAtFilter f →
          DifferentiableAt ℂ (Function.Periodic.cuspFunction h f) 0
-- Mathlib.Topology.Category.Profinite.Basic
Profinite.instInhabited : Inhabited Profinite
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Ideal.comap_minimalPrimes_eq_of_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  Function.Surjective ⇑f → ∀ (I : Ideal S), (Ideal.comap f I).minimalPrimes = Ideal.comap f '' I.minimalPrimes
-- Lean.Server.References
/-- Whether `lake setup-file` has failed for this worker. `none` if no setup info has been received
for this version yet.
 -/
Lean.Server.TransientWorkerILean.isSetupFailure? : Lean.Server.TransientWorkerILean → Option Bool
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.id_def : ∀ {α : Type u₁} (X : CategoryTheory.Discrete α), { down := { down := ⋯ } } = CategoryTheory.CategoryStruct.id X
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.homMk_toHom : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X.toSheafedSpace ⟶ Y.toSheafedSpace)
  (h :
    autoParam
      (∀ (x : ↑X.toTopCat), IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f.hom x)))
      AlgebraicGeometry.LocallyRingedSpace.homMk._auto_1),
  (AlgebraicGeometry.LocallyRingedSpace.homMk f h).toHom = f.hom