mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.toAlgHom_comp : ∀ {R : CommRingCat} {A B C : CategoryTheory.Under R} (f : A ⟶ B) (g : B ⟶ C),
  CommRingCat.toAlgHom (CategoryTheory.CategoryStruct.comp f g) = (CommRingCat.toAlgHom g).comp (CommRingCat.toAlgHom f)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.filterMap_equiv_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  {f : (a : α) → β a → Bool},
  m.WF → (Std.DHashMap.Raw.filterMap (fun k => Option.guard fun v => f k v) m).Equiv (Std.DHashMap.Raw.filter f m)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoOps.mk.inj : ∀ {mkPureApp : Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr}
  {mkBindApp : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr}
  {isPureApp? : Lean.Expr → Option Lean.Expr}
  {splitMonadApp? : Lean.Expr → Lean.Elab.TermElabM (Option (Lean.Elab.Do.MonadInfo × Lean.Expr))}
  {mkMonadApp : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr}
  {mkPureApp_1 : Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr}
  {mkBindApp_1 : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr}
  {isPureApp?_1 : Lean.Expr → Option Lean.Expr}
  {splitMonadApp?_1 : Lean.Expr → Lean.Elab.TermElabM (Option (Lean.Elab.Do.MonadInfo × Lean.Expr))}
  {mkMonadApp_1 : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr},
  { mkPureApp := mkPureApp, mkBindApp := mkBindApp, isPureApp? := isPureApp?, splitMonadApp? := splitMonadApp?,
        mkMonadApp := mkMonadApp } =
      { mkPureApp := mkPureApp_1, mkBindApp := mkBindApp_1, isPureApp? := isPureApp?_1,
        splitMonadApp? := splitMonadApp?_1, mkMonadApp := mkMonadApp_1 } →
    mkPureApp = mkPureApp_1 ∧
      mkBindApp = mkBindApp_1 ∧
        isPureApp? = isPureApp?_1 ∧ splitMonadApp? = splitMonadApp?_1 ∧ mkMonadApp = mkMonadApp_1
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Empty.0.Std.IterM.forIn'_eq_match_step.match_1.splitter : {γ : Type u_1} →
  (motive : ForInStep γ → Sort u_2) →
    (__do_lift : ForInStep γ) →
      ((c : γ) → motive (ForInStep.yield c)) → ((c : γ) → motive (ForInStep.done c)) → motive __do_lift
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.tensorUnit_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Mon C)).X =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.withMVarContextImp : {α : Type} → Lean.MVarId → Lean.MetaM α → Lean.MetaM α
-- Init.Data.List.Zip
List.zipWithAll_map_right : ∀ {α : Type u_1} {β β' : Type u_2} {γ : Type u_3} {l₁ : List α} {l₂ : List β} {f : β → β'}
  {g : Option α → Option β' → γ},
  List.zipWithAll g l₁ (List.map f l₂) = List.zipWithAll (fun a b => g a (f <$> b)) l₁ l₂
-- Init.Omega.Coeffs
/-- Shim for `IntList.gcd`.  -/
Lean.Omega.Coeffs.gcd : Lean.Omega.Coeffs → ℕ
-- Init.Data.List.Perm
_private.Init.Data.List.Perm.0.List.getLast?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.FieldTheory.NormalizedTrace
Algebra.normalizedTrace_algebraMap_apply_eq_self : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [inst_3 : CharZero F]
  [inst_4 : Algebra.IsIntegral F K] (a : F), (Algebra.normalizedTrace F K) ((algebraMap F K) a) = a
-- Mathlib.Topology.Algebra.Group.Quotient
/-- The quotient of a second countable additive topological group by a subgroup is second
countable.  -/
QuotientAddGroup.instSecondCountableTopology : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] (N : AddSubgroup G)
  [SecondCountableTopology G], SecondCountableTopology (G ⧸ N)
-- Init.Data.UInt.Bitwise
UInt16.shiftRight_or : ∀ {a b c : UInt16}, (a ||| b) >>> c = a >>> c ||| b >>> c
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.indicator_summable : ∀ {α : Type u_1} {f : α → NNReal}, Summable f → ∀ (s : Set α), Summable (s.indicator f)
-- Mathlib.Order.Interval.Finset.Fin
Fin.card_Ici : ∀ {n : ℕ} (a : Fin n), (Finset.Ici a).card = n - ↑a
-- Mathlib.Tactic.Positivity.Core
/-- A variation on `assumption` when the hypothesis is `lo ≤ e` where `lo` is a numeral.  -/
Mathlib.Meta.Positivity.compareHypLE : {u : Lean.Level} →
  {α : Q(Type u)} →
    (zα : Q(Zero «$α»)) →
      (pα : Q(PartialOrder «$α»)) →
        (lo e : Q(«$α»)) → Q(«$lo» ≤ «$e») → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e (some pα))
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.liftWith_ReaderT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ρ α : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (f : ({β : Type u} → ReaderT ρ m β → m β) → m α),
  ⦃fun s => (Std.Do.wp (f fun {β} x => x.run s)).apply (fun a => Q.1 a s, Q.2)⦄ MonadControl.liftWith f ⦃Q⦄
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.norm_inr : ∀ {R : Type u_3} {M : Type u_4} [inst : SeminormedRing R] [inst_1 : SeminormedAddCommGroup M] (m : M),
  ‖TrivSqZeroExt.inr m‖ = ‖m‖
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.Extension.congr_simp : ∀ (k : Type u_1) [inst : Field k] (p p_1 : ℕ) (e_p : p = p_1) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP k p]
  (n n_1 : ℕ), n = n_1 → FiniteField.Extension k p n = FiniteField.Extension k p_1 n_1
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.Hom.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P Q : CategoryTheory.Idempotents.Karoubi C}
  {f : P.X ⟶ Q.X}
  {comm :
    autoParam (CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp f Q.p) = f)
      CategoryTheory.Idempotents.Karoubi.Hom.comm._autoParam}
  {f_1 : P.X ⟶ Q.X}
  {comm_1 :
    autoParam (CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp f_1 Q.p) = f_1)
      CategoryTheory.Idempotents.Karoubi.Hom.comm._autoParam},
  { f := f, comm := comm } = { f := f_1, comm := comm_1 } → f = f_1
-- Std.Time.Format.Modifier
Std.Time.instReprOffsetZ.repr : Std.Time.OffsetZ → ℕ → Std.Format
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.lintegral_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {g : β × γ → ENNReal},
  Measurable g → ∫⁻ (c : β × γ), g c ∂(κ.prod η) a = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂η a ∂κ a
-- Mathlib.Algebra.Group.Subgroup.Finsupp
Subgroup.exists_of_mem_closure_range : ∀ {M : Type u_1} [inst : CommGroup M] {ι : Type u_2} (f : ι → M) (x : M) [inst_1 : Fintype ι],
  x ∈ Subgroup.closure (Set.range f) → ∃ a, x = ∏ i, f i ^ a i
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addXYZ_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ≠ Q 0 * P 2 →
            W.addXYZ P Q =
              W.addZ P Q •
                ![W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2)
                    (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                  W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2)
                    (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                  1]
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.exists_variableChange_isCharNeTwoNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [Invertible 2], ∃ C, (C • W).IsCharNeTwoNF
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.unop_sInf : ∀ {G : Type u_2} [inst : AddGroup G] (S : Set (AddSubgroup Gᵃᵒᵖ)), (sInf S).unop = sInf (AddSubgroup.op ⁻¹' S)
-- Mathlib.GroupTheory.Finiteness
Submonoid.powers_fg : ∀ {M : Type u_1} [inst : Monoid M] (r : M), (Submonoid.powers r).FG
-- Init.Data.Float.Float32
/-- Computes the arc tangent (inverse tangent) of `y / x` in radians, in the range `-π`–`π`. The signs
of the arguments determine the quadrant of the result.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`atan2f`.
 -/
Float32.atan2 : Float32 → Float32 → Float32
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.mk_add : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] (x : Submonoid A) (i j : HomogeneousLocalization.NumDenSameDeg 𝒜 x),
  HomogeneousLocalization.mk (i + j) = HomogeneousLocalization.mk i + HomogeneousLocalization.mk j
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.mapₗ_apply_of_measurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β},
  Measurable f → ∀ (μ : MeasureTheory.Measure α), (MeasureTheory.Measure.mapₗ f) μ = MeasureTheory.Measure.map f μ
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.isUnit_iff_eq_bot : ∀ {M : Type u_1} [inst : CommMonoid M] {a : Associates M}, IsUnit a ↔ a = ⊥
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_minKey?_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t → t.minKey?.isSome = true
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_X : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.up α)) (n : α),
  ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.obj K).X.X n = (K.X n).X
-- Lean.Elab.BuiltinNotation
/-- If the term contains any cdots that match the given `HygieneInfo` name (see `isCDotForInfo`),
then returns `some` with the expanded syntax, otherwise returns `none`.

Examples:
- `· + 1` => `fun x => x + 1`
- `f · · b` => `fun x1 x2 => f x1 x2 b`
 -/
Lean.Elab.Term.expandCDot? : Lean.Term → Option Lean.Name → Lean.MacroM (Option Lean.Term)
-- Mathlib.Topology.NhdsWithin
mem_nhdsSet_induced : ∀ {α : Type u_5} {β : Type u_6} {t : TopologicalSpace β} (f : α → β) (s u : Set α),
  u ∈ nhdsSet s ↔ ∃ v ∈ nhdsSet (f '' s), f ⁻¹' v ⊆ u
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.CasesTypes.mk.injEq : ∀ (casesMap casesMap_1 : Lean.PHashMap Lean.Name Bool),
  ({ casesMap := casesMap } = { casesMap := casesMap_1 }) = (casesMap = casesMap_1)
-- Std.Http.Internal.Char
/-- reason-phrase character class:
HTAB / SP / VCHAR
; ASCII-only variant (no obs-text).

Reference: https://httpwg.org/specs/rfc9110.html#reason.phrase
 -/
Std.Http.Internal.Char.reasonPhraseChar : Char → Bool
-- Init.Data.List.Lemmas
List.ext_get : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁.length = l₂.length →
    (∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) → l₁ = l₂
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.supportedEquivFinsupp.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (s : Set M),
  AddMonoidAlgebra.supportedEquivFinsupp s =
    { toFun := fun x => ⟨(↑x).coeff, ⋯⟩, map_add' := ⋯, map_smul' := ⋯,
        invFun := fun x => ⟨AddMonoidAlgebra.ofCoeff ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } ≪≫ₗ
      Finsupp.supportedEquivFinsupp s
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.instCommMonoidWithZero : CommMonoidWithZero Cardinal.{u}
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.ext_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] {f g : M ≃ₜ+ N}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.Algebra.Notation.Support
Pi.mulSupport_mulSingle : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : One M] {i : ι} {a : M} [inst_2 : DecidableEq M],
  Function.mulSupport (Pi.mulSingle i a) = if a = 1 then ∅ else {i}
-- Mathlib.Data.List.MinMax
List.index_of_argmin : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] {f : α → β} [inst_1 : DecidableEq α] {l : List α} {m : α},
  m ∈ List.argmin f l → ∀ {a : α}, a ∈ l → f a ≤ f m → List.idxOf m l ≤ List.idxOf a l
-- Mathlib.CategoryTheory.Grothendieck
/-- Construct an isomorphism in a Grothendieck construction from isomorphisms in its base and fiber.
 -/
CategoryTheory.Grothendieck.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {X Y : CategoryTheory.Grothendieck F} →
        (e₁ : X.base ≅ Y.base) → ((F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber) → (X ≅ Y)
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {X : CategoryTheory.SimplicialObject C} {n : ℕ} {Z : C}
  {x y : AlgebraicTopology.DoldKan.MorphComponents X n Z}, x.a = y.a → x.b = y.b → x = y
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- An analytic function is automatically `C^ω` in a complete space  -/
AnalyticOnNhd.contDiffOn_of_completeSpace : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞} [CompleteSpace F], AnalyticOnNhd 𝕜 f s → ContDiffOn 𝕜 n f s
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Submodule.isCompl_iff_disjoint : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] (s t : Submodule K V),
  Module.finrank K V ≤ Module.finrank K ↥s + Module.finrank K ↥t → (IsCompl s t ↔ Disjoint s t)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.map_id : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent),
  SimpleGraph.ConnectedComponent.map SimpleGraph.Hom.id C = C
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.instCoeForallFormatterAliasValue : Coe (Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter) Lean.PrettyPrinter.Formatter.FormatterAliasValue
-- Mathlib.Order.RelSeries
RelSeries.fromListIsChain_cons : ∀ {α : Type u_1} {r : SetRel α α} (l : List α) (l_ne_nil : l ≠ []) (hl : List.IsChain (fun x1 x2 => (x1, x2) ∈ r) l)
  (x : α) (hx : (x, l.head l_ne_nil) ∈ r),
  RelSeries.fromListIsChain (x :: l) ⋯ ⋯ = (RelSeries.fromListIsChain l l_ne_nil hl).cons x ⋯
-- Mathlib.RingTheory.Ideal.Operations
Ideal.sup_iInf_eq_top : ∀ {R : Type u} [inst : Semiring R] {I : Ideal R} {ι : Type u_1} {s : Finset ι} {J : ι → Ideal R}
  [∀ (i : ι), (J i).IsTwoSided], (∀ i ∈ s, I ⊔ J i = ⊤) → I ⊔ ⨅ i ∈ s, J i = ⊤
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctorCore.map₂_associator : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h))
      (CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h)
        (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h))
        (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)))
-- Mathlib.Algebra.DirectSum.Module
DirectSum.coeLinearMap_lof : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (A : ι → Submodule R M) (i : ι) (x : ↥(A i)),
  (DirectSum.coeLinearMap A) ((DirectSum.lof R ι (fun i => ↥(A i)) i) x) = ↑x
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_diseq_subst1 : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α) (k : ℤ)
  (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.eq_diseq_subst1_cert k p₁ p₂ p₃ = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ = 0 →
      Lean.Grind.Linarith.Poly.denote' ctx p₂ ≠ 0 → Lean.Grind.Linarith.Poly.denote' ctx p₃ ≠ 0
-- Mathlib.Topology.Order.LeftRightNhds
nhds_basis_Ioo_one_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : LinearOrder α] [IsOrderedMonoid α]
  [OrderTopology α] [NoMaxOrder α] (a : α), (nhds a).HasBasis (fun ε => 1 < ε) fun ε => Set.Ioo (a / ε) (a * ε)
-- Mathlib.Data.Num.ZNum
ZNum.div_to_int : ∀ (n d : ZNum), ↑(n / d) = ↑n / ↑d
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.mk.sizeOf_spec : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  [inst_1 : SizeOf I] (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) (i : I)
  (a : D.obj i ⟶ X) (ha : t.app i = CategoryTheory.CategoryStruct.comp a f) (b : D.obj i ⟶ X)
  (hb : t.app i = CategoryTheory.CategoryStruct.comp b f)
  (hab : CategoryTheory.CategoryStruct.comp (c.π.app i) a = CategoryTheory.CategoryStruct.comp (c.π.app i) b)
  (𝒰S : S.OpenCover) [h𝒰S : ∀ (i : 𝒰S.I₀), AlgebraicGeometry.IsAffine (𝒰S.X i)]
  (𝒰X :
    (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S).I₀) →
      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S).X i).OpenCover)
  [h𝒰X :
    ∀ (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S).I₀) (j : (𝒰X i).I₀),
      AlgebraicGeometry.IsAffine ((𝒰X i).X j)],
  sizeOf
      { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := 𝒰S, h𝒰S := h𝒰S, 𝒰X := 𝒰X,
        h𝒰X := h𝒰X } =
    1 + sizeOf c + sizeOf hc + sizeOf i + sizeOf a + sizeOf ha + sizeOf b + sizeOf hb + sizeOf hab + sizeOf 𝒰S
-- Lean.Data.Lsp.Client
Lean.Lsp.RegistrationParams : Type
-- Lean.Parser.Types
Lean.Parser.ParserModuleContext.mk.inj : ∀ {env : Lean.Environment} {options : Lean.Options} {currNamespace : Lean.Name} {openDecls : List Lean.OpenDecl}
  {env_1 : Lean.Environment} {options_1 : Lean.Options} {currNamespace_1 : Lean.Name}
  {openDecls_1 : List Lean.OpenDecl},
  { env := env, options := options, currNamespace := currNamespace, openDecls := openDecls } =
      { env := env_1, options := options_1, currNamespace := currNamespace_1, openDecls := openDecls_1 } →
    env = env_1 ∧ options = options_1 ∧ currNamespace = currNamespace_1 ∧ openDecls = openDecls_1
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.mk.injEq : ∀ {ι : Type u_1} (toPreAbstractSimplicialComplex : PreAbstractSimplicialComplex ι)
  (singleton_mem : ∀ (v : ι), {v} ∈ toPreAbstractSimplicialComplex.faces)
  (toPreAbstractSimplicialComplex_1 : PreAbstractSimplicialComplex ι)
  (singleton_mem_1 : ∀ (v : ι), {v} ∈ toPreAbstractSimplicialComplex_1.faces),
  ({ toPreAbstractSimplicialComplex := toPreAbstractSimplicialComplex, singleton_mem := singleton_mem } =
      { toPreAbstractSimplicialComplex := toPreAbstractSimplicialComplex_1, singleton_mem := singleton_mem_1 }) =
    (toPreAbstractSimplicialComplex = toPreAbstractSimplicialComplex_1)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_update_apply : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ) (a : R) (i : ℕ),
  (p.update n a).coeff i = if i = n then a else p.coeff i
-- Init.Data.Array.Lemmas
Array.not_mem_append : ∀ {α : Type u_1} {a : α} {xs ys : Array α}, a ∉ xs → a ∉ ys → a ∉ xs ++ ys
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Ideal.under_map_of_isLocalizationAtPrime : ∀ {R : Type u_1} [inst : CommSemiring R] (q : Ideal R) [inst_1 : q.IsPrime] {S : Type u_4} [inst_2 : CommSemiring S]
  [inst_3 : Algebra R S] [IsLocalization.AtPrime S q] {p : Ideal R} [p.IsPrime],
  p ≤ q → Ideal.under R (Ideal.map (algebraMap R S) p) = p
-- Mathlib.RingTheory.Localization.Rat
Rat.isFractionRingDen : ∀ (q : ℚ), (↑(IsFractionRing.den ℤ q)).natAbs = q.den
-- Init.Data.List.Sublist
List.Sublist.mem : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, a ∈ l₁ → l₁.Sublist l₂ → a ∈ l₂
-- Init.Data.Array.Attach
Array.countP_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {g : (a : α) → p a → β} {f : β → Bool} {xs : Array α}
  (H₁ : ∀ a ∈ xs, p a),
  Array.countP f (Array.pmap g xs H₁) =
    Array.countP
      (fun x =>
        match x with
        | ⟨a, m⟩ => f (g a ⋯))
      xs.attach
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
lTensor.inverse_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) (y : TensorProduct R Q N),
  (lTensor.inverse Q hfg hg) ((LinearMap.lTensor Q g) y) = Submodule.Quotient.mk y
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
/-- The entropy of `φ '' F` equals the entropy of `F` if `X` is endowed with the pullback by `φ`
of the uniform structure of `Y`.  -/
Dynamics.coverEntropy_image_of_comap : ∀ {X : Type u_1} {Y : Type u_2} (u : UniformSpace Y) {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T → ∀ (F : Set X), Dynamics.coverEntropy T (φ '' F) = Dynamics.coverEntropy S F
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.of_iSup_eq_top : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {ι : Sort u_1}
  (U : ι → ↑Y.affineOpens), ⨆ i, ↑(U i) = ⊤ → (∀ (i : ι), Q (f ∣_ ↑(U i))) → P f
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.norm_integral_le_of_norm_le : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ} {g : ℝ → ℝ},
  a ≤ b →
    (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.Ioc a b → ‖f t‖ ≤ g t) →
      IntervalIntegrable g μ a b → ‖∫ (t : ℝ) in a..b, f t ∂μ‖ ≤ ∫ (t : ℝ) in a..b, g t ∂μ
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.iSup_toSubfield : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Sort u_3} [Nonempty ι]
  (S : ι → IntermediateField F E), (iSup S).toSubfield = ⨆ i, (S i).toSubfield
-- Batteries.Data.List.Scan
List.length_partialSums : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] {l : List α}, l.partialSums.length = l.length + 1
-- Init.Data.SInt.Lemmas
Int8.toISize_toInt16 : ∀ (n : Int8), n.toInt16.toISize = n.toISize
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mkIdInitial_to_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (Y : CategoryTheory.Under X),
  CategoryTheory.Under.Hom.right (CategoryTheory.Under.mkIdInitial.to Y) = Y.hom
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap.0.WeierstrassCurve.termU : Lean.ParserDescr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_eq_get_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} {h : a ∈ t}, t.get a h = (t.get? a).get ⋯