mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- **Alias** of `CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_hom`. -/
CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [inst_3 : G.IsCocontinuous J K]
  [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [inst_5 : G.IsContinuous J K]
  [inst_6 : CategoryTheory.HasWeakSheafify J A] [inst_7 : CategoryTheory.HasWeakSheafify K A]
  (F : CategoryTheory.Functor Dᵒᵖ A),
  ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).hom =
    CategoryTheory.sheafifyLift J (G.op.whiskerLeft (CategoryTheory.toSheafify K F)) ⋯
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.RanIsSheafOfIsCocontinuous.hom_ext : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w}
  [inst_2 : CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C}
  (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A},
  CategoryTheory.Presheaf.IsSheaf J F →
    ∀ {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F}
      (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} {W : A}
      {f g : W ⟶ R.obj (Opposite.op X)},
      (∀ (i : S.Arrow),
          CategoryTheory.CategoryStruct.comp f (R.map i.f.op) = CategoryTheory.CategoryStruct.comp g (R.map i.f.op)) →
        f = g
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_one : ∀ {R : Type u} {M : Type v} [inst : One R] [inst_1 : Zero M], TrivSqZeroExt.snd 1 = 0
-- Mathlib.Algebra.Order.Positive.Ring
Positive.addLeftReflectLE : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : AddLeftStrictMono M] [AddLeftReflectLE M],
  AddLeftReflectLE { x // 0 < x }
-- Mathlib.Algebra.Lie.Weights.Linear
/-- In characteristic zero, the weights of any finite-dimensional Lie module are linear and vanish
on the derived ideal.  -/
LieModule.instLinearWeightsOfCharZero : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] [IsDomain R]
  [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M] [inst_11 : LieRing.IsNilpotent L] [CharZero R],
  LieModule.LinearWeights R L M
-- Init.Prelude
/-- Constructs a `Min` instance from a decidable `≤` operation.
 -/
minOfLe : {α : Type u_1} → [inst : LE α] → [DecidableRel LE.le] → Min α
-- Init.Data.UInt.Lemmas
UInt16.toNat_sub : ∀ (a b : UInt16), (a - b).toNat = (2 ^ 16 - b.toNat + a.toNat) % 2 ^ 16
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- The [binary entropy function](https://en.wikipedia.org/wiki/Binary_entropy_function)
`binEntropy p := - p * log p - (1-p) * log (1 - p)`
is the Shannon entropy of a Bernoulli random variable with success probability `p`.  -/
Real.binEntropy : ℝ → ℝ
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- The path 0 ⟶ 1 in `I`  -/
unitInterval.path01 : Path 0 1
-- Mathlib.NumberTheory.Modular
ModularGroup.lcRow0Extend_apply : ∀ {cd : Fin 2 → ℤ} (hcd : IsCoprime (cd 0) (cd 1)) (f : (i : Fin 2) → (fun a => Fin 2 → ℝ) i) (i a : Fin 2),
  (ModularGroup.lcRow0Extend hcd) f i a =
    (![(LinearMap.GeneralLinearGroup.generalLinearEquiv ℝ (Fin 2 → ℝ))
            (Matrix.GeneralLinearGroup.toLin (Matrix.planeConformalMatrix (↑(cd 0)) (-↑(cd 1)) ⋯)),
          LinearEquiv.refl ℝ (Fin 2 → ℝ)]
        i)
      (f i) a
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_eq_zero_iff : ∀ {R : Type u} [inst : Semiring R] (t : R) (n : ℕ), (Polynomial.monomial n) t = 0 ↔ t = 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.Const.ofList l) k' = some v
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableMul.mk : ∀ {M : Type u_2} [inst : MeasurableSpace M] [inst_1 : Mul M],
  autoParam (∀ (c : M), Measurable fun x => c * x) MeasurableMul.measurable_const_mul._autoParam →
    autoParam (∀ (c : M), Measurable fun x => x * c) MeasurableMul.measurable_mul_const._autoParam → MeasurableMul M
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- If `i : D ⥤ C` is reflective, the inverse functor of `i ≌ F.essImage` can be explicitly
defined by the reflector.  -/
CategoryTheory.equivEssImageOfReflective : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {i : CategoryTheory.Functor D C} → [CategoryTheory.Reflective i] → D ≌ i.EssImageSubcategory
-- Mathlib.Order.Interval.Basic
Interval.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (g : β →o γ) (f : α →o β) (s : Interval α), Interval.map g (Interval.map f s) = Interval.map (g.comp f) s
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.swapRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  ProbabilityTheory.IsZeroOrMarkovKernel κ.swapRight
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.mkOrderEmbedding_apply : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s : Submonoid α}
  (b : ↥s) (a : α), (Localization.mkOrderEmbedding b) a = Localization.mk a b
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂IdIso_inv_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} (α : (CategoryTheory.Functor.id C).comp S ⟶ S.comp (CategoryTheory.Functor.id D))
  (T : D) (β : (CategoryTheory.Functor.id D).obj T ⟶ T)
  (hα :
    autoParam (α = CategoryTheory.CategoryStruct.comp S.leftUnitor.hom S.rightUnitor.inv)
      CategoryTheory.CostructuredArrow.map₂IdIso._auto_1)
  (hβ :
    autoParam (β = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id D).obj T))
      CategoryTheory.CostructuredArrow.map₂IdIso._auto_3)
  (X : CategoryTheory.CostructuredArrow S T),
  ((CategoryTheory.CostructuredArrow.map₂IdIso α T β hα hβ).inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasurableEquiv.quasiMeasurePreserving_symm : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : MeasurableSpace β] (μ : MeasureTheory.Measure α)
  (e : α ≃ᵐ β), MeasureTheory.Measure.QuasiMeasurePreserving (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) μ
-- Mathlib.Algebra.Regular.Pi
Pi.isAddLeftRegular_iff : ∀ {ι : Type u_1} {R : ι → Type u_3} [inst : (i : ι) → Add (R i)] {a : (i : ι) → R i},
  IsAddLeftRegular a ↔ ∀ (i : ι), IsAddLeftRegular (a i)
-- Mathlib.Order.Filter.Defs
Filter.instInfSet : {α : Type u_1} → InfSet (Filter α)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.truncGEδLE.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b), t.truncGEδLE a b h = t.truncGEδLE a b h
-- Mathlib.NumberTheory.WellApproximable
approxAddOrderOf.image_nsmul_subset : ∀ {A : Type u_1} [inst : SeminormedAddCommGroup A] {m : ℕ} (δ : ℝ) (n : ℕ),
  0 < m → (fun y => m • y) '' approxAddOrderOf A (n * m) δ ⊆ approxAddOrderOf A n (↑m * δ)
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabWaitForExpectedType : Lean.Elab.Term.TermElab
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.posterior_prod_id_comp : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω],
  (μ.bind ⇑κ).bind ⇑((ProbabilityTheory.posterior κ μ).prod ProbabilityTheory.Kernel.id) = μ.compProd κ
-- Mathlib.Algebra.Group.Defs
exists_zpow_surjective : ∀ (G : Type u_2) [inst : Pow G ℤ] [IsCyclic G], ∃ g, Function.Surjective fun x => g ^ x
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.inv_mul_cancel : ∀ {k : Type u_2} [inst : Field k] (φ : PowerSeries k), PowerSeries.constantCoeff φ ≠ 0 → φ⁻¹ * φ = 1
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.IsCovering.costar_bijective : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] {φ : U ⥤q V},
  φ.IsCovering → ∀ (u : U), Function.Bijective (φ.costar u)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Rxo.instFinite : ∀ {α : Type u} {β : α → Type v} [inst : Ord α], Std.Iterators.Finite (Std.DTreeMap.Internal.RxoIterator α β) Id
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_two_pi_sub : ∀ (x : ℂ), Complex.cos (2 * ↑Real.pi - x) = Complex.cos x
-- Mathlib.Analysis.InnerProductSpace.OfNorm
InnerProductSpaceable.add_left : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [InnerProductSpaceable E] (x y z : E), inner_✝ 𝕜 (x + y) z = inner_✝ 𝕜 x z + inner_✝ 𝕜 y z
-- Mathlib.NumberTheory.LucasLehmer
/-- We define `ω = 2 + √3`.  -/
LucasLehmer.X.ω : {q : ℕ} → LucasLehmer.X q
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.mk.inj : ∀ {α₁ : Type w} {m : Type w → Type w'} {β₁ : Type w} {inst : Std.Iterator α₁ m β₁} {α₂ β₂ : Type w}
  {left : Std.IterM m β₁} {memoizedLeft : Option { out // ∃ it, it.IsPlausibleOutput out }} {right : Std.IterM m β₂}
  {left_1 : Std.IterM m β₁} {memoizedLeft_1 : Option { out // ∃ it, it.IsPlausibleOutput out }}
  {right_1 : Std.IterM m β₂},
  { left := left, memoizedLeft := memoizedLeft, right := right } =
      { left := left_1, memoizedLeft := memoizedLeft_1, right := right_1 } →
    left = left_1 ∧ memoizedLeft = memoizedLeft_1 ∧ right = right_1
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- Evaluates a TM2 program to completion, with the output on the same stack as the input.  -/
Turing.TM2.eval : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        [Inhabited Λ] →
          [DecidableEq K] → [Inhabited σ] → (Λ → Turing.TM2.Stmt Γ Λ σ) → (k : K) → List (Γ k) → Part (List (Γ k))
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.mapRange.linearMap.eq_1 : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9}
  [inst_1 : (i : ι) → AddCommMonoid (β₁ i)] [inst_2 : (i : ι) → AddCommMonoid (β₂ i)]
  [inst_3 : (i : ι) → Module R (β₁ i)] [inst_4 : (i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i),
  DFinsupp.mapRange.linearMap f = { toFun := DFinsupp.mapRange (fun i x => (f i) x) ⋯, map_add' := ⋯, map_smul' := ⋯ }
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.done : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Category.Ring.Constructions
/-- The explicit cocone with tensor products as the fibered product in `CommRingCat`.  -/
CommRingCat.pushoutCocone : (R A B : Type u) →
  [inst : CommRing R] →
    [inst_1 : CommRing A] →
      [inst_2 : CommRing B] →
        [inst_3 : Algebra R A] →
          [inst_4 : Algebra R B] →
            CategoryTheory.Limits.PushoutCocone (CommRingCat.ofHom (algebraMap R A))
              (CommRingCat.ofHom (algebraMap R B))
-- Lean.Data.PersistentArray
Lean.PersistentArray.findSomeRevMAux : {α : Type u} →
  {m : Type v → Type w} → [Monad m] → {β : Type v} → (α → m (Option β)) → Lean.PersistentArrayNode α → m (Option β)
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.degree_divX_lt : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → p.divX.degree < p.degree
-- Init.Data.String.Slice
String.Slice.SplitIterator.atEnd.sizeOf_spec : ∀ {σ : String.Slice → Type} {ρ : Type} {pat : ρ} {s : String.Slice}
  [inst : String.Slice.Pattern.ToForwardSearcher pat σ] [inst_1 : (a : String.Slice) → SizeOf (σ a)]
  [inst_2 : SizeOf ρ], sizeOf String.Slice.SplitIterator.atEnd = 1
-- Std.Data.ExtDTreeMap.Basic
/-- Updates the values of the map by applying the given function to all mappings, keeping
only those mappings where the function returns `some` value.
 -/
Std.ExtDTreeMap.filterMap : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} →
      {cmp : α → α → Ordering} → ((a : α) → β a → Option (γ a)) → Std.ExtDTreeMap α β cmp → Std.ExtDTreeMap α γ cmp
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.prodMk : ∀ {α : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} [inst : CommMonoid α] [inst_1 : CommMonoid β₁] [inst_2 : CommMonoid β₂]
  {A : Set α} {B₁ : Set β₁} {B₂ : Set β₂} {f₁ : α → β₁} {f₂ : α → β₂} {n : ℕ},
  IsMulFreimanHom n A B₁ f₁ → IsMulFreimanHom n A B₂ f₂ → IsMulFreimanHom n A (B₁ ×ˢ B₂) fun x => (f₁ x, f₂ x)
-- Mathlib.CategoryTheory.Monoidal.Action.End
/-- When `C` acts on the right on `D`, the functor `curriedAction : C ⥤ (D ⥤ D)`
is monoidal, where `D ⥤ D` has the composition monoidal structure.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] →
            (CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D).Monoidal
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.prodMkLeft_compProd : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {Ω'' : Type u_3} {mΩ'' : MeasurableSpace Ω''} {Y : Ω'' → ℝ} {cY : NNReal}
  {η : ProbabilityTheory.Kernel Ω Ω''},
  ProbabilityTheory.Kernel.HasSubgaussianMGF Y cY η (ν.bind ⇑κ) →
    ProbabilityTheory.Kernel.HasSubgaussianMGF Y cY (ProbabilityTheory.Kernel.prodMkLeft Ω' η) (ν.compProd κ)
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyoneda_map_app_shrinkCoyonedaObjObjEquiv_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X X' : Cᵒᵖ}
  {Y : C} (f : Opposite.unop X ⟶ Y) (g : X ⟶ X'),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.map g).app Y))
      (CategoryTheory.shrinkCoyonedaObjObjEquiv.symm f) =
    CategoryTheory.shrinkCoyonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g.unop f)
-- Mathlib.Order.UpperLower.Basic
/-- **Alias** of the reverse direction of `isUpperSet_preimage_ofDual_iff`. -/
IsLowerSet.toDual : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsLowerSet s → IsUpperSet (⇑OrderDual.ofDual ⁻¹' s)
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.algHom_ext' : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {f : M →ₗ[R] N},
  IsBaseChange S f →
    ∀ {Q : Type u_3} [inst_9 : AddCommMonoid Q] [inst_10 : Module S Q] [inst_11 : Module R Q]
      [inst_12 : IsScalarTower R S Q] (g₁ g₂ : N →ₗ[S] Q), ↑R g₁ ∘ₗ f = ↑R g₂ ∘ₗ f → g₁ = g₂
-- Mathlib.Algebra.Field.ULift
ULift.semifield : {α : Type u} → [Semifield α] → Semifield (ULift.{u_1, u} α)
-- Init.Data.Slice.Array.Iterator
/-- `Subarray` representation.  -/
Array.Subarray.repr : {α : Type u} → [Repr α] → Subarray α → Std.Format
-- Mathlib.Analysis.Calculus.DSlope
pow_sub_smul_iterate_dslope_of_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} (n : ℕ),
  (∀ k < n, (Function.swap dslope a)^[k] f a = 0) → ∀ (b : 𝕜), (b - a) ^ n • (Function.swap dslope a)^[n] f b = f b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblZ_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R) (u : R),
  W'.dblZ (u • P) = u ^ 4 * W'.dblZ P
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.discreteEquiv.eq_1 : ∀ {α : Type u₁},
  CategoryTheory.discreteEquiv =
    { toFun := CategoryTheory.Discrete.as, invFun := CategoryTheory.Discrete.mk, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.BitVec.Lemmas
BitVec.toInt_ofBool : ∀ (b : Bool), (BitVec.ofBool b).toInt = -b.toInt
-- Mathlib.Tactic.IrreducibleDef
/-- Executes the commands,
and stops after the first error.
In short, S-A-F-E.
 -/
_private.Mathlib.Tactic.IrreducibleDef.0.Lean.Elab.Command.commandStop_at_first_error__ : Lean.ParserDescr
-- Std.Time.Format.Modifier
/-- `Number` represents different number formatting styles.
 -/
Std.Time.Number : Type
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_pow : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : CommSemiring S] (f : R →+* S) (x : S)
  (n : ℕ), Polynomial.eval₂ f x (p ^ n) = Polynomial.eval₂ f x p ^ n
-- Mathlib.Util.Export
_private.Mathlib.Util.Export.0.Lean.Export.exportDef.ind : List Lean.Name → Lean.ExportM Unit
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.Suggestion.mk : Lean.Name → Float → Option String → Lean.LibrarySuggestions.Suggestion
-- Std.Http.Data.URI.Encoding
/-- Attempts to create an `EncodedString` from a `ByteArray`. Returns `some` if the byte array contains only
valid encoded characters and all percent signs are followed by exactly two hex digits, `none` otherwise.
 -/
Std.Http.URI.EncodedString.ofByteArray? : {r : UInt8 → Bool} → ByteArray → Option (Std.Http.URI.EncodedString r)
-- Mathlib.Order.Filter.Basic
Filter.exists_mem_subset_iff : ∀ {α : Type u} {f : Filter α} {s : Set α}, (∃ t ∈ f, t ⊆ s) ↔ s ∈ f
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α} {v : β}, Std.ExtDHashMap.Const.get! (m.insert k v) k = v
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Std.Iterators.Types.ArrayIterator.instIterator.eq_1 : ∀ {m : Type w → Type w'} {α : Type w} [inst : Pure m],
  Std.Iterators.Types.ArrayIterator.instIterator =
    {
      IsPlausibleStep := fun it x =>
        match x with
        | Std.IterStep.yield it' out =>
          it.internalState.array = it'.internalState.array ∧
            it'.internalState.pos = it.internalState.pos + 1 ∧
              ∃ (x : it.internalState.pos < it.internalState.array.size),
                it.internalState.array[it.internalState.pos] = out
        | Std.IterStep.skip it => False
        | Std.IterStep.done => it.internalState.pos ≥ it.internalState.array.size,
      step := fun it =>
        pure
          (Std.Shrink.deflate
            (if h : it.internalState.pos < it.internalState.array.size then
              Std.PlausibleIterStep.yield
                { internalState := { array := it.internalState.array, pos := it.internalState.pos + 1 } }
                it.internalState.array[it.internalState.pos] ⋯
            else Std.PlausibleIterStep.done ⋯)) }
-- Lean.Parser.Extension
Lean.Parser.ParserResolution.parser.inj : ∀ {decl : Lean.Name} {isDescr : Bool} {decl_1 : Lean.Name} {isDescr_1 : Bool},
  Lean.Parser.ParserResolution.parser decl isDescr = Lean.Parser.ParserResolution.parser decl_1 isDescr_1 →
    decl = decl_1 ∧ isDescr = isDescr_1
-- Mathlib.Order.Bounded
Set.bounded_le_Ioc : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Set.Bounded (fun x1 x2 => x1 ≤ x2) (Set.Ioc a b)
-- Init.Data.List.Basic
List.and_cons : ∀ {a : Bool} {l : List Bool}, (a :: l).and = (a && l.and)
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.mutuallySingular_of_mutuallySingular_compProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} {ξ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η],
  (μ.compProd κ).MutuallySingular (ν.compProd η) →
    ξ.AbsolutelyContinuous μ → ξ.AbsolutelyContinuous ν → ∀ᵐ (x : α) ∂ξ, (κ x).MutuallySingular (η x)
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.isTriangulated_of_precomp : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.HasShift D ℤ] [inst_5 : CategoryTheory.HasShift E ℤ]
  (F : CategoryTheory.Functor C D) [inst_6 : F.CommShift ℤ] (G : CategoryTheory.Functor D E) [inst_7 : G.CommShift ℤ]
  [inst_8 : CategoryTheory.Limits.HasZeroObject C] [inst_9 : CategoryTheory.Limits.HasZeroObject D]
  [inst_10 : CategoryTheory.Limits.HasZeroObject E] [inst_11 : CategoryTheory.Preadditive C]
  [inst_12 : CategoryTheory.Preadditive D] [inst_13 : CategoryTheory.Preadditive E]
  [inst_14 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_15 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
  [inst_16 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive] [inst_17 : CategoryTheory.Pretriangulated C]
  [inst_18 : CategoryTheory.Pretriangulated D] [inst_19 : CategoryTheory.Pretriangulated E] [(F.comp G).IsTriangulated]
  [F.IsTriangulated] [F.mapArrow.EssSurj], G.IsTriangulated
-- Lean.Compiler.IR.Basic
Lean.IR.Param.x : Lean.IR.Param → Lean.IR.VarId
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.HasSubobjectClassifier.χ.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasSubobjectClassifier C] {U X : C}
  (m m_1 : U ⟶ X) (e_m : m = m_1) [inst_2 : CategoryTheory.Mono m],
  CategoryTheory.HasSubobjectClassifier.χ m = CategoryTheory.HasSubobjectClassifier.χ m_1
-- Mathlib.Analysis.RCLike.Lemmas
RCLike.conjCLE_norm : ∀ {K : Type u_1} [inst : RCLike K], ‖↑RCLike.conjCLE‖ = 1
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.instInitialOppositeRightOpOfFinal : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor Cᵒᵖ D) [F.Final], F.rightOp.Initial
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesIsoX₂_hom_inv_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] (hf : S.f = 0) {Z : C} (h : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.opcyclesIsoX₂ hf).hom (CategoryTheory.CategoryStruct.comp S.pOpcycles h) = h
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
TensorProduct.eq_zero_of_fg_of_subtype_eq_zero : ∀ {R : Type u} {M : Type u_1} {N : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {P : Submodule R M},
  P.FG →
    ∀ {t : TensorProduct R (↥P) N},
      (LinearMap.rTensor N P.subtype) t = 0 →
        ∃ Q, ∃ (hPQ : P ≤ Q), Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = 0