mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivWithinAt.hcongr_24 : ∀ (𝕜 𝕜' : Type u_1),
  𝕜 = 𝕜' →
    ∀ (inst : NontriviallyNormedField 𝕜) (inst' : NontriviallyNormedField 𝕜'),
      inst ≍ inst' →
        ∀ (E E' : Type u_2),
          E = E' →
            ∀ (inst_1 : NormedAddCommGroup E) (inst'_1 : NormedAddCommGroup E'),
              inst_1 ≍ inst'_1 →
                ∀ (inst_2 : NormedSpace 𝕜 E) (inst'_2 : NormedSpace 𝕜' E'),
                  inst_2 ≍ inst'_2 →
                    ∀ (H H' : Type u_3),
                      H = H' →
                        ∀ (inst_3 : TopologicalSpace H) (inst'_3 : TopologicalSpace H'),
                          inst_3 ≍ inst'_3 →
                            ∀ (I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜' E' H'),
                              I ≍ I' →
                                ∀ (M M' : Type u_4),
                                  M = M' →
                                    ∀ (inst_4 : TopologicalSpace M) (inst'_4 : TopologicalSpace M'),
                                      inst_4 ≍ inst'_4 →
                                        ∀ (inst_5 : ChartedSpace H M) (inst'_5 : ChartedSpace H' M'),
                                          inst_5 ≍ inst'_5 →
                                            ∀ (E'_1 E'' : Type u_5),
                                              E'_1 = E'' →
                                                ∀ (inst_6 : NormedAddCommGroup E'_1) (inst'_6 : NormedAddCommGroup E''),
                                                  inst_6 ≍ inst'_6 →
                                                    ∀ (inst_7 : NormedSpace 𝕜 E'_1) (inst'_7 : NormedSpace 𝕜' E''),
                                                      inst_7 ≍ inst'_7 →
                                                        ∀ (H'_1 H'' : Type u_6),
                                                          H'_1 = H'' →
                                                            ∀ (inst_8 : TopologicalSpace H'_1)
                                                              (inst'_8 : TopologicalSpace H''),
                                                              inst_8 ≍ inst'_8 →
                                                                ∀ (I'_1 : ModelWithCorners 𝕜 E'_1 H'_1)
                                                                  (I'' : ModelWithCorners 𝕜' E'' H''),
                                                                  I'_1 ≍ I'' →
                                                                    ∀ (M'_1 M'' : Type u_7),
                                                                      M'_1 = M'' →
                                                                        ∀ (inst_9 : TopologicalSpace M'_1)
                                                                          (inst'_9 : TopologicalSpace M''),
                                                                          inst_9 ≍ inst'_9 →
                                                                            ∀ (inst_10 : ChartedSpace H'_1 M'_1), ⋯
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the first commutative square of a triangle morphism  -/
CategoryTheory.Pretriangulated.TriangleMorphism.comm₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} (self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂)
  {Z : C} (h : T₂.obj₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp T₁.mor₁ (CategoryTheory.CategoryStruct.comp self.hom₂ h) =
    CategoryTheory.CategoryStruct.comp self.hom₁ (CategoryTheory.CategoryStruct.comp T₂.mor₁ h)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Unitization.quasispectrum_eq_spectrum_inr' : ∀ (R : Type u_3) (S : Type u_4) {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Algebra R S] [inst_4 : Module S A] [inst_5 : IsScalarTower S A A] [inst_6 : SMulCommClass S A A]
  [inst_7 : Module R A] [inst_8 : IsScalarTower R S A] (a : A), quasispectrum R a = spectrum R ↑a
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
/-- **Alias** of `MeasureTheory.NullSingletonClass`.

---

Measure `μ` has value zero on singletons.  -/
MeasureTheory.NoAtoms : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Prop
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.subset_hull : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] {s : Set E}, s ⊆ ↑(PointedCone.hull R s)
-- Mathlib.CategoryTheory.Elements
/-- The opposite of the category of elements of a presheaf of types
is equivalent to a category of costructured arrows for the Yoneda embedding functor.  -/
CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type (max w v))) →
      F.Elementsᵒᵖ ≌ CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda.{w, v, u} F
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.coe_toContinuousMapHom : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : CommSemiring R] [inst_4 : IsTopologicalSemiring R] [inst_5 : StarRing R] [inst_6 : ContinuousStar R],
  ⇑ContinuousMapZero.toContinuousMapHom = toContinuousMap
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.BalancedAtRoot.adjust_left : ∀ {l l' r : ℕ},
  Std.DTreeMap.Internal.Impl.BalancedAtRoot l r →
    l - 1 ≤ l' →
      l' ≤ l + 1 →
        Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l' r ∨ Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r l'
-- Init.Data.List.Lemmas
List.flatten_filter_ne_nil : ∀ {α : Type u_1} [inst : DecidablePred fun l => l ≠ []] {L : List (List α)},
  (List.filter (fun l => decide (l ≠ [])) L).flatten = L.flatten
-- Mathlib.Topology.NhdsWithin
/-- If `L` and `R` are neighborhoods of `b` within sets whose union is `Set.univ`, then
`L ∪ R` is a neighborhood of `b`.  -/
union_mem_nhds_of_mem_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {b : α} {I₁ I₂ : Set α},
  Set.univ = I₁ ∪ I₂ → ∀ {L : Set α}, L ∈ nhdsWithin b I₁ → ∀ {R : Set α}, R ∈ nhdsWithin b I₂ → L ∪ R ∈ nhds b
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddCommSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddCommSemigroup α],
  OrderDual.instAddCommSemigroup = { toAddSemigroup := OrderDual.instAddSemigroup, add_comm := ⋯ }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.fold_eq_foldl_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {δ : Type w} {β : Type v} {m : Std.DHashMap α fun x => β}
  {f : δ → α → β → δ} {init : δ},
  Std.DHashMap.fold f init m = List.foldl (fun a b => f a b.1 b.2) init (Std.DHashMap.Const.toList m)
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.uniqueToTop : {X : Type u} → [inst : Preorder X] → [inst_1 : OrderTop X] → {x : X} → Unique (x ⟶ ⊤)
-- Mathlib.Logic.Relation
/-- **Alias** of `Relation.reflTransGen_le_of_le`. -/
Relation.reflTransGen_of_transitive_reflexive : ∀ {α : Type u_1} {r r' : α → α → Prop} [Std.Refl r] [IsTrans α r], r' ≤ r → Relation.ReflTransGen r' ≤ r
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.syntaxVal : ℤ → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.sub_one_right_of_dvd : ∀ {R : Type u} [inst : CommRing R] {x y : R}, x ∣ y → IsCoprime x (y - 1)
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.sub_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → ∀ (c : F), InnerProductSpace.HarmonicContOnCl (f - fun x => c) s
-- Mathlib.Topology.ContinuousOn
ContinuousAt.continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ContinuousAt f x → ContinuousWithinAt f s x
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- **Alias** of `MeasureTheory.integral_inter_add_sdiff₀`. -/
MeasureTheory.integral_inter_add_diff₀ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasureTheory.NullMeasurableSet t μ →
    MeasureTheory.IntegrableOn f s μ → ∫ (x : X) in s ∩ t, f x ∂μ + ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.Algebra.Divisibility.Basic
dvd_of_mul_left_dvd : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b c : α}, a * b ∣ c → b ∣ c
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseMarkerLong : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.HourMarker
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : Inhabited β] {a : α},
  Std.DTreeMap.Const.get! ∅ a = default
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_left_surjective : ∀ {x : ℝ}, x ≠ 0 → Function.Surjective fun y => y ^ x
-- Mathlib.FieldTheory.IntermediateField.Basic
toIntermediateField'_toSubalgebra : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  S.toIntermediateField' ⋯ = S
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
trdeg_pos : ∀ (R : Type u_3) (A : Type v) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.Transcendental R A], 0 < Algebra.trdeg R A
-- Mathlib.Algebra.Lie.Basic
lie_self : ∀ {L : Type v} [inst : LieRing L] (x : L), ⁅x, x⁆ = 0
-- Mathlib.Algebra.GroupWithZero.Conj
GroupWithZero.isConj_iff₀ : ∀ {α : Type u_1} [inst : GroupWithZero α] {a b : α}, IsConj a b ↔ ∃ c, c ≠ 0 ∧ c * a * c⁻¹ = b
-- Mathlib.Order.BooleanAlgebra.Set
Set.disjoint_sdiff_right : ∀ {α : Type u_1} {s t : Set α}, Disjoint s (t \ s)
-- Mathlib.Tactic.Positivity.Core
/-- A variation on `assumption` when the hypothesis is `x = e` where `x` is a numeral.  -/
Mathlib.Meta.Positivity.compareHypEq : {u : Lean.Level} →
  {α : Q(Type u)} →
    (zα : Q(Zero «$α»)) →
      (pα : Q(PartialOrder «$α»)) →
        (e x : Q(«$α»)) → Q(«$x» = «$e») → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e (some pα))
-- Lean.Attributes
Lean.throwAttrNotInAsyncCtx : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → {α : Type} → Lean.Name → Lean.Name → Option Lean.Name → m α
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The meromorphic function of `s` which agrees with
`Gamma (s / 2) * π ^ (-s / 2) * ∑' n : ℕ, cos (2 * π * a * n) / n ^ s` for `1 < re s`.
 -/
HurwitzZeta.completedCosZeta : UnitAddCircle → ℂ → ℂ
-- Mathlib.Analysis.Normed.Operator.Conformal
/-- A continuous linear map `f'` is said to be conformal if it's
a nonzero multiple of a linear isometry.  -/
IsConformalMap : {R : Type u_1} →
  {X : Type u_2} →
    {Y : Type u_3} →
      [inst : NormedField R] →
        [inst_1 : SeminormedAddCommGroup X] →
          [inst_2 : SeminormedAddCommGroup Y] →
            [inst_3 : NormedSpace R X] → [inst_4 : NormedSpace R Y] → (X →L[R] Y) → Prop
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.rightComm_tmul : ∀ (R : Type uR) {S : Type uS} (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : Semiring B] [inst_2 : Algebra R B] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module B M]
  [inst_6 : IsScalarTower R B M] [inst_7 : AddCommMonoid P] [inst_8 : AddCommMonoid Q] [inst_9 : Module R Q]
  [inst_10 : CommSemiring S] [inst_11 : Module S M] [inst_12 : Module S P] [inst_13 : Algebra S B]
  [inst_14 : IsScalarTower S B M] [inst_15 : SMulCommClass R S M] [inst_16 : SMulCommClass S R M] (m : M) (p : P)
  (q : Q), (TensorProduct.AlgebraTensorModule.rightComm R S B M P Q) (m ⊗ₜ[S] p ⊗ₜ[R] q) = m ⊗ₜ[R] q ⊗ₜ[S] p
-- Mathlib.Analysis.Analytic.Composition
/-- The first coefficient of a composition of formal multilinear series is the composition of the
first coefficients seen as continuous linear maps.  -/
FormalMultilinearSeries.comp_coeff_one : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : AddCommGroup G] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] [inst_6 : Module 𝕜 G]
  [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalSpace G]
  [inst_10 : IsTopologicalAddGroup E] [inst_11 : ContinuousConstSMul 𝕜 E] [inst_12 : IsTopologicalAddGroup F]
  [inst_13 : ContinuousConstSMul 𝕜 F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜 G]
  (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (v : Fin 1 → E),
  (q.comp p 1) v = (q 1) fun _i => (p 1) v
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.comap_eq_generateFrom : ∀ {α : Type u_1} {β : Type u_2} (m : MeasurableSpace β) (f : α → β),
  MeasurableSpace.comap f m = MeasurableSpace.generateFrom {t | ∃ s, MeasurableSet s ∧ f ⁻¹' s = t}
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_filterMapM_filterMapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → n (Option γ)} {g : γ → o (Option δ)} {it : Std.IterM m β},
  (Std.IterM.filterMapM g (Std.IterM.filterMapM f it)).toList =
    (Std.IterM.filterMapM
        (fun b => do
          let __do_lift ← liftM (f b)
          match __do_lift with
            | none => pure none
            | some fb => g fb)
        it).toList
-- Mathlib.Topology.Algebra.Order.Field
Filter.Tendsto.inv_tendsto_atTop : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f : α → 𝕜},
  Filter.Tendsto f l Filter.atTop → Filter.Tendsto f⁻¹ l (nhds 0)
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_int_eq_ascFactorial : ∀ (a b : ℕ), Polynomial.eval (↑a + ↑b) (descPochhammer ℤ b) = ↑((a + 1).ascFactorial b)
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.instEvalExprReduceConfig : Lean.Elab.ConfigEval.EvalExpr Lean.Meta.Command.ReduceConfig
-- Mathlib.Combinatorics.Matroid.Circuit
/-- **Alias** of `Matroid.IsCircuit.sdiff_singleton_isBasis`. -/
Matroid.IsCircuit.diff_singleton_isBasis : ∀ {α : Type u_1} {M : Matroid α} {C : Set α} {e : α}, M.IsCircuit C → e ∈ C → M.IsBasis (C \ {e}) C
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.liftP_iff_of_isUniform : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F],
  MvQPF.IsUniform →
    ∀ {α : TypeVec.{u} n} (x : F α) (p : (i : Fin2 n) → α i → Prop),
      MvFunctor.LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ MvFunctor.supp x i, p i u
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.addLeft.eq_1 : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddLeftMono α] (a : α),
  OrderIso.addLeft a = { toEquiv := Equiv.addLeft a, map_rel_iff' := ⋯ }
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Abelian.Ext.mapExactFunctor_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : CategoryTheory.HasExt C]
  [inst_8 : CategoryTheory.HasExt D] (X Y : C) (n : ℕ) (f g : CategoryTheory.Abelian.Ext X Y n),
  CategoryTheory.Abelian.Ext.mapExactFunctor F (f + g) =
    CategoryTheory.Abelian.Ext.mapExactFunctor F f + CategoryTheory.Abelian.Ext.mapExactFunctor F g
-- Mathlib.RingTheory.Coalgebra.Basic
CommSemiring.comul_apply : ∀ (R : Type u) [inst : CommSemiring R] (r : R), CoalgebraStruct.comul r = 1 ⊗ₜ[R] r
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factors_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} {P : CategoryTheory.Subobject Y}, P.Factors 0
-- Mathlib.LinearAlgebra.Projection
LinearMap.ofIsCompl_apply_right : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (h : IsCompl p q) {φ : ↥p →ₗ[R] F}
  {ψ : ↥q →ₗ[R] F} (v : ↥q), (LinearMap.ofIsCompl h φ ψ) ↑v = ψ v
-- Mathlib.Data.ZMod.Basic
ZMod.val_cast_eq_val_of_lt : ∀ {m n : ℕ} [nzm : NeZero m] {a : ZMod m}, a.val < n → a.cast.val = a.val
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_erase_le_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  t.erase k ≠ ∅ → ∀ {fallback : α}, (cmp ((t.erase k).maxKeyD fallback) (t.maxKeyD fallback)).isLE = true
-- Init.MetaTypes
Lean.Meta.ExtractLetsConfig.mk.inj : ∀
  {proofs types implicits descend underBinder usedOnly merge useContext onlyGivenNames preserveBinderNames lift proofs_1
    types_1 implicits_1 descend_1 underBinder_1 usedOnly_1 merge_1 useContext_1 onlyGivenNames_1 preserveBinderNames_1
    lift_1 : Bool},
  { proofs := proofs, types := types, implicits := implicits, descend := descend, underBinder := underBinder,
        usedOnly := usedOnly, merge := merge, useContext := useContext, onlyGivenNames := onlyGivenNames,
        preserveBinderNames := preserveBinderNames, lift := lift } =
      { proofs := proofs_1, types := types_1, implicits := implicits_1, descend := descend_1,
        underBinder := underBinder_1, usedOnly := usedOnly_1, merge := merge_1, useContext := useContext_1,
        onlyGivenNames := onlyGivenNames_1, preserveBinderNames := preserveBinderNames_1, lift := lift_1 } →
    proofs = proofs_1 ∧
      types = types_1 ∧
        implicits = implicits_1 ∧
          descend = descend_1 ∧
            underBinder = underBinder_1 ∧
              usedOnly = usedOnly_1 ∧
                merge = merge_1 ∧
                  useContext = useContext_1 ∧
                    onlyGivenNames = onlyGivenNames_1 ∧ preserveBinderNames = preserveBinderNames_1 ∧ lift = lift_1
-- Lean.Compiler.IR.Basic
Lean.IR.instReprVarId : Repr Lean.IR.VarId
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.le_inf_support_coeff_finsetProd : ∀ {R : Type u_1} {A : Type u_3} {T : Type u_4} {ι : Type u_6} [inst : SemilatticeInf T] [inst_1 : OrderTop T]
  [inst_2 : CommSemiring R] [inst_3 : AddCommMonoid A] [inst_4 : AddCommMonoid T] [AddLeftMono T] [AddRightMono T]
  {degt : A → T},
  0 ≤ degt 0 →
    (∀ (a b : A), degt a + degt b ≤ degt (a + b)) →
      ∀ (s : Finset ι) (f : ι → AddMonoidAlgebra R A),
        ∑ i ∈ s, (f i).coeff.support.inf degt ≤ (∏ i ∈ s, f i).coeff.support.inf degt
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_one_right : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (m n : ℕ), f.resultant 1 m n = f.coeff m ^ n
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.Option.instDecidableEq.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (val : α) (h_1 : Unit → motive none)
  (h_2 : (val : α) → motive (some val)),
  (match some val with
    | none => h_1 ()
    | some val => h_2 val) =
    h_2 val
-- Mathlib.CategoryTheory.Abelian.Basic
/-- Any abelian category has pullbacks  -/
CategoryTheory.Abelian.hasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C],
  CategoryTheory.Limits.HasPullbacks C
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.trim_eq_iInf : ∀ {α : Type u_1} [inst : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (s : Set α),
  m.trim s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.const_smul : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : NormedRing 𝕜] [inst_2 : (i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] {f : (i : α) → E i},
  Memℓp f p → ∀ (c : 𝕜), Memℓp (c • f) p
-- Mathlib.Algebra.CharP.Quotient
CharP.quotient : ∀ (R : Type u_1) [inst : CommRing R] (p : ℕ) [hp1 : Fact (Nat.Prime p)], ↑p ∈ nonunits R → CharP (R ⧸ Ideal.span {↑p}) p
-- Init.Control.Lawful.MonadAttach.Lemmas
WeaklyLawfulMonadAttach.pbind_eq_bind : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] {x : m α} {f : α → m β}, (MonadAttach.pbind x fun a x => f a) = x >>= f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k a : α} {h' : a ∈ t.erase k}, Std.ExtDTreeMap.Const.get (t.erase k) a h' = Std.ExtDTreeMap.Const.get t a ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₆_of_isCharTwoJEqZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF], W.c₆ = -216 * W.b₆
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.toPretrivialization_injective : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z], Function.Injective fun e => e.toPretrivialization
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_sdiff_lt_sum_sdiff : ∀ {ι : Type u_9} {M : Type u_10} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M]
  [inst_3 : DecidableEq ι] {s t : Finset ι} {f : ι → M},
  ∑ i ∈ s \ t, f i < ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i < ∑ i ∈ t, f i
-- Init.Data.SInt.Lemmas
Int8.ofIntLE_int64ToInt : ∀ (x : Int64) {h₁ : Int8.minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ Int8.maxValue.toInt},
  Int8.ofIntLE x.toInt h₁ h₂ = x.toInt8
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.nonsingularLift_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [Nontrivial R], W'.NonsingularLift ⟦![0, 1, 0]⟧
-- Mathlib.Algebra.Polynomial.Lifts
Polynomial.mem_lifts : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} (p : Polynomial S),
  p ∈ Polynomial.lifts f ↔ ∃ q, Polynomial.map f q = p
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.eq_append_of_dropPrefix?_slice_eq_some : ∀ {pat s res : String.Slice}, s.dropPrefix? pat = some res → s.copy = pat.copy ++ res.copy
-- Mathlib.CategoryTheory.Groupoid
/-- In a groupoid, isomorphisms are equivalent to morphisms.  -/
CategoryTheory.Groupoid.isoEquivHom : {C : Type u} → [inst : CategoryTheory.Groupoid C] → (X Y : C) → (X ≅ Y) ≃ (X ⟶ Y)
-- Mathlib.Algebra.Field.Subfield.Basic
/-- `RingHom.rangeRestrictField` as a `RingEquiv`.
 -/
RingHom.rangeRestrictFieldEquiv : {K : Type u} → {L : Type v} → [inst : DivisionRing K] → [inst_1 : DivisionRing L] → (f : K →+* L) → K ≃+* ↥f.fieldRange
-- Mathlib.Algebra.Group.Units.Hom
/-- If two homomorphism from a group to a monoid are equal at `x`, then they are equal at `x⁻¹`.  -/
eq_on_inv : ∀ {F : Type u_1} {G : Type u_2} {M : Type u_3} [inst : Group G] [inst_1 : Monoid M] [inst_2 : FunLike F G M]
  [MonoidHomClass F G M] (f g : F) {x : G}, f x = g x → f x⁻¹ = g x⁻¹
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.symm_monoidHomCongrRight : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [inst : MulOneClass M] [inst_1 : CommMonoid N₁]
  [inst_2 : CommMonoid N₂] (e : N₁ ≃* N₂), e.monoidHomCongrRight.symm = e.symm.monoidHomCongrRight