mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {h : (t.get? k).isSome = true}, (t.get? k).get h = t.get k ⋯
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.range_fst : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S],
  NonUnitalRingHom.srange (NonUnitalRingHom.fst R S) = ⊤
-- Std.Sat.AIG.Basic
Std.Sat.AIG.denote.go : {α : Type} →
  (x : ℕ) → (decls : Array (Std.Sat.AIG.Decl α)) → (α → Bool) → x < decls.size → Std.Sat.AIG.IsDAG α decls → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (t : CategoryTheory.Limits.PullbackCone f g) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp t.fst (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp t.snd (CategoryTheory.CategoryStruct.comp g h)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α},
  (a == b) = true → Std.Internal.List.getEntry? a l = Std.Internal.List.getEntry? b l
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f g : PseudoEpimorphism α β},
  f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
fderiv_continuousLinearEquiv_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {G' : Type u_5} [inst_7 : NormedAddCommGroup G']
  [inst_8 : NormedSpace 𝕜 G'] (L : G ≃L[𝕜] G') (f : E → F →L[𝕜] G) (x : E),
  fderiv 𝕜 (fun x => ↑L ∘SL f x) x = ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderiv 𝕜 f x
-- Init.Data.Bool
Bool.not_bne : ∀ (a b : Bool), ((!a) != b) = !a != b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasMultiplicativeReduction.multiplicativeReduction : ∀ {R : Type u_1} {inst : CommRing R} {inst_1 : IsDomain R} {inst_2 : IsDiscreteValuationRing R} {K : Type u_2}
  {inst_3 : Field K} {inst_4 : Algebra R K} {inst_5 : IsFractionRing R K} {W : WeierstrassCurve K}
  [self : WeierstrassCurve.HasMultiplicativeReduction R W],
  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.c₄ = 1
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.reduce.eq_1 : ∀ (u : PNat.XgcdType), u.reduce = if x : u.r = 0 then u.finish else u.step.reduce.flip
-- Lean.Meta.SizeOf
Lean.Meta.mkSizeOfSpecLemmaName : Lean.Name → Lean.Name
-- Mathlib.RingTheory.Valuation.LocalSubring
/-- [Stacks Tag 00IB](https://stacks.math.columbia.edu/tag/00IB) -/
LocalSubring.exists_valuationRing_of_isMax : ∀ {K : Type u_3} [inst : Field K] {R : LocalSubring K}, IsMax R → ∃ R', R'.toLocalSubring = R
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_single_eq_of_ne : ∀ {n : Type u_10} {α : Type u_12} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : AddCommMonoid α] (i j : n)
  (c : α), i ≠ j → (Matrix.single i j c).trace = 0
-- Mathlib.Analysis.Convex.Function
OrderIso.concaveOn_symm : ∀ {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid α]
  [inst_3 : PartialOrder α] [inst_4 : SMul 𝕜 α] [inst_5 : AddCommMonoid β] [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 β]
  (f : α ≃o β), ConvexOn 𝕜 Set.univ ⇑f → ConcaveOn 𝕜 Set.univ ⇑f.symm
-- Mathlib.Algebra.Category.ModuleCat.Products
/-- The coproduct cone induced by the concrete coproduct.  -/
ModuleCat.coproductCocone : {R : Type u} → [inst : Ring R] → {ι : Type v} → (Z : ι → ModuleCat R) → [DecidableEq ι] → CategoryTheory.Limits.Cofan Z
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.whisker_right_comp : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b c d : B} {f f' : CategoryTheory.FreeBicategory.Hom a b} (g : CategoryTheory.FreeBicategory.Hom b c)
  (h : CategoryTheory.FreeBicategory.Hom c d) (η : CategoryTheory.FreeBicategory.Hom₂ f f'),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.toPresheaf_preservesColimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (J : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] [CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat],
  CategoryTheory.Limits.PreservesColimitsOfShape J (PresheafOfModules.toPresheaf R)
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- The *Euler Product* for a multiplicative arithmetic function `f` with values in a
complete normed commutative ring `R`: if `‖f ·‖` is summable, then
`∏' p : Nat.Primes, ∑' e, f (p ^ e) = ∑' n, f n`.  -/
ArithmeticFunction.IsMultiplicative.eulerProduct_tprod : ∀ {R : Type u_1} [inst : NormedCommRing R] [CompleteSpace R] {f : ArithmeticFunction R},
  f.IsMultiplicative → (Summable fun x => ‖f x‖) → ∏' (p : Nat.Primes), ∑' (e : ℕ), f (↑p ^ e) = ∑' (n : ℕ), f n
-- Mathlib.Algebra.Ring.CompTypeclasses
/-- The ring homomorphism is surjective  -/
RingHomSurjective.is_surjective : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {inst : Semiring R₁} {inst_1 : Semiring R₂} {σ : R₁ →+* R₂}
  [self : RingHomSurjective σ], Function.Surjective ⇑σ
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_eq_iff_eq_sq : ∀ {x y : ℝ}, 0 ≤ x → 0 ≤ y → (√x = y ↔ x = y ^ 2)
-- Mathlib.LinearAlgebra.Projectivization.Collinear
Projectivization.isCollinear_subsingleton : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (S : Set (Projectivization K V)), S.Subsingleton → Projectivization.IsCollinear S
-- Mathlib.CategoryTheory.Monoidal.Transport
/-- Analogous to `CategoryTheory.LaxMonoidalFunctor.εIso`  -/
CategoryTheory.Monoidal.InducingFunctorData.εIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategoryStruct D] →
            {F : CategoryTheory.Functor D C} →
              CategoryTheory.Monoidal.InducingFunctorData F →
                (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ≅
                  F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.sections.ext_iff : ∀ {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)}
  {x y : I.sections}, x = y ↔ x.val = y.val
-- Lean.Elab.Do.ForwardSyntax
Lean.Elab.Do.ForwardArg.mk.sizeOf_spec : ∀ (binders : Array (Lean.TSyntax `Lean.Parser.Term.funBinder)) (body : Lean.DoSeq),
  sizeOf { binders := binders, body := body } = 1 + sizeOf binders + sizeOf body
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.flip_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (A : LinearMap.BilinForm R M) (x y : M), ((LinearMap.BilinForm.flipHom A) x) y = (A y) x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.smulRight_zero : ∀ {M₁ : Type u_4} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁] {M₂ : Type u_6}
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] {R : Type u_9} {S : Type u_10} [inst_4 : Semiring R]
  [inst_5 : Semiring S] [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module R S] [inst_9 : Module S M₂]
  [inst_10 : IsScalarTower R S M₂] [inst_11 : TopologicalSpace S] [inst_12 : ContinuousSMul S M₂] (f : M₁ →L[R] S),
  f.smulRight 0 = 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.instZero : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        [inst : Ring k] →
          [inst_1 : AddCommGroup V1] →
            [inst_2 : Module k V1] →
              [inst_3 : AddTorsor V1 P1] → [inst_4 : AddCommGroup V2] → [inst_5 : Module k V2] → Zero (P1 →ᵃ[k] V2)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] [inst_3 : SizeOf C] (X : C) [commRingObj : CategoryTheory.CommRingObj X],
  sizeOf { X := X, commRingObj := commRingObj } = 1 + sizeOf X + sizeOf commRingObj
-- Lean.Data.Lsp.Client
Lean.Lsp.Registration.mk : String → String → Option Lean.Json → Lean.Lsp.Registration
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_iff : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {v : ι → M},
  LinearIndepOn R v s ↔ ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0
-- Lean.Widget.InteractiveCode
/-- Tags pretty-printed code with infos from the delaborator.  -/
Lean.Widget.tagCodeInfos : Lean.Elab.ContextInfo →
  Lean.SubExpr.PosMap Lean.Elab.Info → Lean.Widget.TaggedText (ℕ × ℕ) → BaseIO Lean.Widget.CodeWithInfos
-- Mathlib.Analysis.RCLike.Basic
RCLike.imLm_coe : ∀ {K : Type u_1} [inst : RCLike K], ⇑RCLike.imLm = ⇑RCLike.im
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.hom_comp : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z),
  TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (TopCat.Hom.hom g).comp (TopCat.Hom.hom f)
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.Config.mk.inj : ∀ {transparency : Lean.Meta.TransparencyMode} {occs : Lean.Meta.Occurrences}
  {castMode : Mathlib.Tactic.DepRewrite.CastMode} {castTransparency transparency_1 : Lean.Meta.TransparencyMode}
  {occs_1 : Lean.Meta.Occurrences} {castMode_1 : Mathlib.Tactic.DepRewrite.CastMode}
  {castTransparency_1 : Lean.Meta.TransparencyMode},
  { transparency := transparency, occs := occs, castMode := castMode, castTransparency := castTransparency } =
      { transparency := transparency_1, occs := occs_1, castMode := castMode_1,
        castTransparency := castTransparency_1 } →
    transparency = transparency_1 ∧ occs = occs_1 ∧ castMode = castMode_1 ∧ castTransparency = castTransparency_1
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_injective : ∀ {R : Type u_1} {a b : R} [inst : Zero R], Function.Injective QuadraticAlgebra.C
-- Init.Data.Int.Pow
Int.neg_pow : ∀ {m : ℤ} {n : ℕ}, (-m) ^ n = (-1) ^ (n % 2) * m ^ n
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.forget₁_mapId : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : CategoryTheory.Bicategory.Adj B),
  CategoryTheory.Bicategory.Adj.forget₁.mapId x = CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.id x).l
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} [inst_1 : SizeOf C] [inst_2 : SizeOf ι]
  (hom : (i : ι) → D₁.obj i ⟶ D₂.obj i)
  (comm :
    autoParam
      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
        (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
        CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (hom i₁)) (D₂.hom q f₁ f₂ ⋯ ⋯) =
          CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (hom i₂)))
      CategoryTheory.Pseudofunctor.DescentData.Hom.comm._autoParam),
  sizeOf { hom := hom, comm := comm } = 1
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mk.inj : ∀ {ι : Type u_1} {V : Type u} {inst : CategoryTheory.Category.{v, u} V} {inst_1 : CategoryTheory.Preadditive V}
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} {hom : (i j : ι) → C.X i ⟶ D.X j}
  {zero : autoParam (∀ (i j : ι), ¬c.Rel j i → hom i j = 0) Homotopy.zero._autoParam}
  {comm : autoParam (∀ (i : ι), f.f i = (dNext i) hom + (prevD i) hom + g.f i) Homotopy.comm._autoParam}
  {hom_1 : (i j : ι) → C.X i ⟶ D.X j}
  {zero_1 : autoParam (∀ (i j : ι), ¬c.Rel j i → hom_1 i j = 0) Homotopy.zero._autoParam}
  {comm_1 : autoParam (∀ (i : ι), f.f i = (dNext i) hom_1 + (prevD i) hom_1 + g.f i) Homotopy.comm._autoParam},
  { hom := hom, zero := zero, comm := comm } = { hom := hom_1, zero := zero_1, comm := comm_1 } → hom = hom_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α}
  {k k' : α},
  cmp k k' = Ordering.eq →
    k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertManyIfNewUnit l).getKey? k' = some k
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsRatStieltjesPoint.iInf_rat_gt_eq : ∀ {α : Type u_1} {f : α → ℚ → ℝ} {a : α}, ProbabilityTheory.IsRatStieltjesPoint f a → ∀ (t : ℚ), ⨅ r, f a ↑r = f a t
-- Mathlib.CategoryTheory.Limits.Filtered
/-- `C` is cofiltered if and only if for every functor `F : J ⥤ C` from a finite category there is
some `X : C` such that `lim Hom(X, F·)` is nonempty.  -/
CategoryTheory.IsCofiltered.iff_nonempty_limit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.IsCofiltered C ↔
    ∀ {J : Type v} [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
      (F : CategoryTheory.Functor J C),
      ∃ X, Nonempty (CategoryTheory.Limits.limit (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))))
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.mk : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : MeasureTheory.SignedMeasure α} {μ : MeasureTheory.Measure α},
  s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ →
    s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ → s.HaveLebesgueDecomposition μ
-- Mathlib.RingTheory.Localization.Defs
isLocalization_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S],
  IsLocalization M S ↔
    (∀ (y : ↥M), IsUnit ((algebraMap R S) ↑y)) ∧
      (∀ (z : S), ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1) ∧
        ∀ {x y : R}, (algebraMap R S) x = (algebraMap R S) y → ∃ c, ↑c * x = ↑c * y
-- Mathlib.RingTheory.ClassGroup.Basic
/-- If the class group is trivial, any integral ideal that is a unit as a fractional ideal
is principal.  -/
ClassGroup.isPrincipal_of_isUnit_coeIdeal : ∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [inst_4 : IsDomain R] [Subsingleton (ClassGroup R)] (I : Ideal R), IsUnit ↑I → Submodule.IsPrincipal I
-- Lean.Data.Lsp.Basic
Lean.Lsp.PartialResultParams.partialResultToken? : Lean.Lsp.PartialResultParams → Option Lean.Lsp.ProgressToken
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
CategoryTheory.Initial.mono_to : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (B : C) [CategoryTheory.MonoidalClosed C],
  CategoryTheory.Mono (CategoryTheory.Limits.initial.to B)
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.instIsCocontinuousOverLeftIteratedSliceForwardOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (f : CategoryTheory.Over X), f.iteratedSliceForward.IsCocontinuous ((J.over X).over f) (J.over f.left)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₈_of_isCharTwoJNeZeroNF_of_char_two : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] [CharP R 2], W.b₈ = W.a₆
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.norm_integral_le_of_norm_le_const' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R C : ℝ},
  (∀ z ∈ Metric.sphere c |R|, ‖f z‖ ≤ C) → ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * Real.pi * |R| * C
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapNatIso_functor_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T')
  {Y X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T} (f : Y ⟶ X),
  ((CategoryTheory.StructuredArrow.mapNatIso i).functor.map f).right = f.right
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toArray_rcc_eq_fallback : ∀ {m n fallback : ℤ} {i : ℕ}, (n + 1 - m).toNat ≤ i → (m...=n).toArray.getD i fallback = fallback
-- Mathlib.Computability.RegularExpressions
RegularExpression.star_rmatch_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (P : RegularExpression α) (x : List α),
  P.star.rmatch x = true ↔ ∃ S, x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
-- Mathlib.Topology.MetricSpace.IsometricSMul
edist_neg_neg : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G]
  (a b : G), edist (-a) (-b) = edist a b
-- Mathlib.RingTheory.Ideal.Maps
Ideal.mem_comap : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] {f : F}
  {K : Ideal S} [inst_3 : RingHomClass F R S] {x : R}, x ∈ Ideal.comap f K ↔ f x ∈ K
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.inr_pushoutAssoc_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂)
  (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂]
  [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂))
      g₄]
  [inst_4 :
    CategoryTheory.Limits.HasPushout g₁
      (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.inr
        (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
      (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₃ g₄)
      (CategoryTheory.Limits.pushout.inr g₁
        (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] {U V : (TopologicalSpace.Opens ↑↑X)ᵒᵖ} (i : U ⟶ V),
  CategoryTheory.CategoryStruct.comp (X.presheaf.map i)
      (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f (Opposite.unop V)) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f (Opposite.unop U))
      (Y.presheaf.map ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).op.map i))
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α} {fallback : Unit},
  (Std.TreeMap.Raw.unitOfList l cmp).getD k fallback = ()
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.instInvolutiveNeg.eq_1 : ∀ {α : Type u} [inst : InvolutiveNeg α], WithZero.instInvolutiveNeg = { toNeg := WithZero.instNeg, neg_neg := ⋯ }
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_add_of_lt : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.toWithBotSyn (m.withBotDegree g) < m.toWithBotSyn (m.withBotDegree f) → m.withBotDegree (f + g) = m.withBotDegree f
-- Init.Data.Nat.Lcm
Nat.lcm_pos_iff : ∀ {m n : ℕ}, 0 < m.lcm n ↔ 0 < m ∧ 0 < n
-- Mathlib.Order.Interval.Finset.Basic
Finset.card_Ioo_eq_card_Icc_sub_two : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  (Finset.Ioo a b).card = (Finset.Icc a b).card - 2
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.baseChange_dblZ : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Jacobian R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).dblZ (⇑f ∘ P) = f ((W'.baseChange A).dblZ P)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.inaccessible.injEq : ∀ (e e_1 : Lean.Expr), (Lean.Meta.Match.Pattern.inaccessible e = Lean.Meta.Match.Pattern.inaccessible e_1) = (e = e_1)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasDerivWithinAt.const_cpow : ∀ {f : ℂ → ℂ} {s : Set ℂ} {f' x c : ℂ},
  HasDerivWithinAt f f' s x → c ≠ 0 ∨ f x ≠ 0 → HasDerivWithinAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') s x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₂ → Std.DHashMap.Const.get? (m₁.union m₂) k = Std.DHashMap.Const.get? m₁ k
-- Lean.Attributes
Lean.AttrM : Type → Type
-- Mathlib.Topology.Algebra.Module.Equiv
/-- An extensionality lemma for `R ≃L[R] M`.  -/
ContinuousLinearEquiv.ext₁ : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] {f g : R₁ ≃L[R₁] M₁}, f 1 = g 1 → f = g
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flipping_inverse_obj_obj_map : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor D (CategoryTheory.Functor C E)) (k : C) {X Y : D} (f : X ⟶ Y),
  ((CategoryTheory.Functor.flipping.inverse.obj F).obj k).map f = (F.map f).app k
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- The unique map to the terminal object.  -/
CategoryTheory.SemiCartesianMonoidalCategory.toUnit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory C] →
      (X : C) → X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.Tactic.LinearCombination
Mathlib.Tactic.LinearCombination.Expanded.proof.sizeOf_spec : ∀ (rel : Mathlib.Ineq) (pf : Lean.Term),
  sizeOf (Mathlib.Tactic.LinearCombination.Expanded.proof rel pf) = 1 + sizeOf rel + sizeOf pf
-- Init.Data.Slice.Operations
Std.Slice.SliceSize.mk : {γ : Type u} → (Std.Slice γ → ℕ) → Std.Slice.SliceSize γ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_of_lt_of_lt_one' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b c : α}, b < c → a < 1 → b * a < c
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coeff_sub' : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddGroup R] (x y : HahnSeries Γ R),
  (x - y).coeff = x.coeff - y.coeff
-- Lean.Compiler.IR.Basic
Lean.IR.VarIdSet : Type