mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  {inst_1 : LinearOrder J} {inst_2 : SuccOrder J} {inst_3 : OrderBot J}
  {inst_4 : CategoryTheory.Limits.HasIterationOfShape J C} {inst_5 : WellFoundedLT J} {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iic j)) C} {obj_bot : F.obj ⟨⊥, ⋯⟩ = Φ.X₀}
  {arrowSucc_eq :
    ∀ (i : J) (hi : i < j), CategoryTheory.SmallObject.SuccStruct.arrowSucc F i hi = Φ.toSuccArrow (F.obj ⟨i, ⋯⟩)}
  {arrowMap_limit :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i),
      CategoryTheory.SmallObject.SuccStruct.arrowMap F k i ⋯ hij =
        CategoryTheory.SmallObject.SuccStruct.arrowι (CategoryTheory.SmallObject.restrictionLT F hij) hi k hk}
  {F_1 : CategoryTheory.Functor (↑(Set.Iic j)) C} {obj_bot_1 : F_1.obj ⟨⊥, ⋯⟩ = Φ.X₀}
  {arrowSucc_eq_1 :
    ∀ (i : J) (hi : i < j), CategoryTheory.SmallObject.SuccStruct.arrowSucc F_1 i hi = Φ.toSuccArrow (F_1.obj ⟨i, ⋯⟩)}
  {arrowMap_limit_1 :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i),
      CategoryTheory.SmallObject.SuccStruct.arrowMap F_1 k i ⋯ hij =
        CategoryTheory.SmallObject.SuccStruct.arrowι (CategoryTheory.SmallObject.restrictionLT F_1 hij) hi k hk},
  { F := F, obj_bot := obj_bot, arrowSucc_eq := arrowSucc_eq, arrowMap_limit := arrowMap_limit } =
      { F := F_1, obj_bot := obj_bot_1, arrowSucc_eq := arrowSucc_eq_1, arrowMap_limit := arrowMap_limit_1 } →
    F = F_1
-- Mathlib.Data.List.Basic
List.flatMap_pure_eq_map : ∀ {α : Type u} {β : Type v} (f : α → β) (l : List α), List.flatMap (pure ∘ f) l = List.map f l
-- Mathlib.Data.List.GetD
List.getD_eq_getElem : ∀ {α : Type u} (l : List α) (d : α) {n : ℕ} (hn : n < l.length), l.getD n d = l[n]
-- Mathlib.GroupTheory.CosetCover
/-- A vector space over an infinite field cannot be a finite union of proper subspaces.  -/
Subspace.biUnion_ne_univ_of_top_notMem : ∀ {k : Type u_1} {E : Type u_2} [inst : DivisionRing k] [Infinite k] [inst_2 : AddCommGroup E] [inst_3 : Module k E]
  {s : Finset (Subspace k E)}, ⊤ ∉ s → ⋃ p ∈ s, ↑p ≠ Set.univ
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indepSet_empty_right : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ] (s : Set Ω),
  ProbabilityTheory.Kernel.IndepSet s ∅ κ μ
-- Lean.Meta.Tactic.Grind.Anchor
/-- Hashes names for computing anchors (aka stable hash codes)
 -/
_private.Lean.Meta.Tactic.Grind.Anchor.0.Lean.Meta.Grind.hashName : Lean.Name → UInt64
-- Mathlib.Analysis.Calculus.Gradient.Basic
toDual_comp_gradient : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜}, ⇑(InnerProductSpace.toDual 𝕜 F) ∘ gradient f = fderiv 𝕜 f
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.compl_def : ∀ {R : Type u} {M : Type v} [inst : Group R] [inst_1 : MulAction R M] (s : SubMulAction R M), sᶜ.carrier = (↑s)ᶜ
-- Init.Data.Rat.Lemmas
Rat.eq_iff_mul_eq_mul : ∀ {p q : ℚ}, p = q ↔ p.num * ↑q.den = q.num * ↑p.den
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The function from a given commutative ring in the diagram to the colimit commutative ring.  -/
CommRingCat.Colimits.coconeFun : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) → (j : J) → ↑(F.obj j) → CommRingCat.Colimits.ColimitType F
-- Mathlib.Topology.Sheaves.Functors
TopCat.Sheaf.instIsRightAdjointPushforward : ∀ {X Y : TopCat} (f : X ⟶ Y) (A : Type u_1) [inst : CategoryTheory.Category.{w, u_1} A] {FA : A → A → Type u_2}
  {CA : A → Type w} [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_2 : CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.HasColimits A]
  [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
  [(CategoryTheory.forget A).ReflectsIsomorphisms], (TopCat.Sheaf.pushforward A f).IsRightAdjoint
-- Mathlib.Algebra.Category.ModuleCat.Images
/-- The corestriction map to the image  -/
ModuleCat.factorThruImage : {R : Type u} → [inst : Ring R] → {G H : ModuleCat R} → (f : G ⟶ H) → G ⟶ ModuleCat.image f
-- Mathlib.Algebra.Module.CharacterModule
/-- Given `n : ℕ`, the map `m ↦ m / n`.  -/
CharacterModule.int.divByNat : ℕ → CharacterModule.int
-- Mathlib.Control.Functor.Multivariate
/-- Multivariate functors, i.e. functor between the category of type vectors
and the category of Type  -/
MvFunctor : {n : ℕ} → (TypeVec.{u_2} n → Type u_1) → Type (max u_1 (u_2 + 1))
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.toCycles_i_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology j] {Z : C}
  (h : K.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.toCycles i j) (CategoryTheory.CategoryStruct.comp (K.iCycles j) h) =
    CategoryTheory.CategoryStruct.comp (K.d i j) h
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.map_map : ∀ {R : Type u} [inst : CommRing R] (C : WeierstrassCurve.VariableChange R) {A : Type v} [inst_1 : CommRing A]
  (φ : R →+* A) {B : Type w} [inst_2 : CommRing B] (ψ : A →+* B), (C.map φ).map ψ = C.map (ψ.comp φ)
-- Std.Do.PostCond
Std.Do.ExceptConds.snd_true : ∀ {ε : Type u} {ps : Std.Do.PostShape}, Std.Do.ExceptConds.true.2 = Std.Do.ExceptConds.true
-- Init.Data.BitVec.Lemmas
BitVec.clzAuxRec_zero : ∀ {w : ℕ} (x : BitVec w), x.clzAuxRec 0 = if x.getLsbD 0 = true then BitVec.ofNat w (w - 1) else BitVec.ofNat w w
-- Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
Ideal.finite_minimalPrimes_of_isNoetherianRing : ∀ (R : Type u_1) [inst : CommSemiring R] [hR : IsNoetherianRing R] (I : Ideal R), I.minimalPrimes.Finite
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.repr_smul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {G : Type u_5} [inst_3 : Group G] [inst_4 : DistribMulAction G M] [inst_5 : SMulCommClass G R M] (g : G)
  (b : Module.Basis ι R M), (g • b).repr = (DistribMulAction.toLinearEquiv R M g).symm ≪≫ₗ b.repr
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instCartesianMonoidalCategoryScheme : CategoryTheory.CartesianMonoidalCategory AlgebraicGeometry.Scheme
-- Mathlib.Algebra.Group.Equiv.Opposite
MulOpposite.opMulEquiv_symm_apply : ∀ {M : Type u_1} [inst : CommMonoid M] (a : Mᵐᵒᵖ), MulOpposite.opMulEquiv.symm a = MulOpposite.unop a
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.balanced_glue : ∀ {α : Type u} {β : α → Type v} {l r : Std.DTreeMap.Internal.Impl α β} {hl : l.Balanced} {hr : r.Balanced}
  {hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size}, (l.glue r hl hr hlr).Balanced
-- Mathlib.Topology.Constructible
Topology.IsConstructible.empty : ∀ {X : Type u_2} [inst : TopologicalSpace X], Topology.IsConstructible ∅
-- Lean.Attributes
Lean.throwAttrDeclInImportedModule : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → {α : Type} → Lean.Name → Lean.Name → m α
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.rankOne_def : ∀ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x : E) (y : F),
  ((InnerProductSpace.rankOne 𝕜) x) y = ((innerSL 𝕜) y).smulRight x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.continuous_cos : Continuous Real.cos
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch.mk : ∀ {pat s : ByteArray} {needlePos stackPos : ℕ} (stackPos_le_size : stackPos ≤ s.size)
  (needlePos_le_size : needlePos ≤ pat.size) (needlePos_le_stackPos : needlePos ≤ stackPos),
  (∀ (j : ℕ) (hj : j < needlePos), pat[j] = s[stackPos - needlePos + j]) →
    String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s needlePos stackPos
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- The interior of any C¹ manifold is open.

This is currently only proven for C¹ manifolds, but holds at least for finite-dimensional
topological manifolds too; see `ModelWithCorners.isInteriorPoint_iff_of_mem_atlas`.  -/
ModelWithCorners.isOpen_interior : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M],
  n ≠ 0 → IsOpen (ModelWithCorners.interior M)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
measurable_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [CompleteSpace F] [inst_4 : MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜]
  [inst_6 : MeasurableSpace F] [BorelSpace F] (f : 𝕜 → F), Measurable (deriv f)
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.isPositive_toLinearMap_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E), (↑T).IsPositive ↔ T.IsPositive
-- Std.Time.Zoned.Database.PosixTz
_private.Std.Time.Zoned.Database.PosixTz.0.Std.Time.TimeZone.quotedName : Std.Internal.Parsec.String.Parser String
-- Mathlib.RingTheory.Etale.Locus
Algebra.etaleLocus_eq_univ_iff_etale : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FinitePresentation R A], Algebra.etaleLocus R A = Set.univ ↔ Algebra.Etale R A
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.coeff_Ψ₂Sq_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 4 ≠ 0 → W.Ψ₂Sq.coeff 3 ≠ 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_of_mem_keys : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m.keys → k ∈ m
-- Lean.Meta.Iterator
/-- Convert a list into an iterator with the current state.
 -/
Lean.Meta.Iterator.ofList : {α : Type} → List α → Lean.MetaM (Lean.Meta.Iterator α)
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.injective_codRestrict_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {q : Submodule R₂ M₂} {f : M →ₛₗ[τ₁₂] M₂} (hf : ∀ (x : M), f x ∈ q),
  Function.Injective ⇑(LinearMap.codRestrict q f hf) ↔ Function.Injective ⇑f
-- Init.Data.BitVec.Lemmas
BitVec.getElem_concat : ∀ {w : ℕ} (x : BitVec w) (b : Bool) (i : ℕ) (h : i < w + 1), (x.concat b)[i] = if h : i = 0 then b else x[i - 1]
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.mulAction.eq_1 : ∀ {M' : Type u_1} {α : Type u_2} [inst : Monoid M'] [inst_1 : MulAction M' α] (S : Submonoid M'),
  S.mulAction = inferInstance
-- Mathlib.CategoryTheory.Opposites
/-- An equivalence between categories gives an equivalence between the opposite categories.
 -/
CategoryTheory.Equivalence.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (C ≌ D) → (Cᵒᵖ ≌ Dᵒᵖ)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
_private.Mathlib.RingTheory.Extension.Presentation.Submersive.0.Algebra.PreSubmersivePresentation.jacobiMatrix_comp_inl_inl : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.PreSubmersivePresentation S T ι' σ')
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_7 : Fintype σ] [inst_8 : Fintype σ'] (i j : σ'),
  (MvPolynomial.aeval (Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ P.val)))
      ((Q.comp P).jacobiMatrix (Sum.inl j) (Sum.inl i)) =
    Q.jacobiMatrix j i
-- Plausible.Shrinkable
Plausible.UInt16.shrinkable : Plausible.Shrinkable UInt16
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castLE_Ici_castLE : ∀ {m n : ℕ} (i : Fin m) (h : m ≤ n), Fin.castLE h ⁻¹' Set.Ici (Fin.castLE h i) = Set.Ici i
-- Mathlib.Topology.EMetricSpace.Defs
Metric.exists_eball_subset_eball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal},
  y ∈ Metric.eball x ε → ∃ ε' > 0, Metric.eball y ε' ⊆ Metric.eball x ε
-- Std.Async.System
/-- The ID of the group.
 -/
Std.Async.System.GroupInfo.groupId : Std.Async.System.GroupInfo → Std.Async.System.GroupId
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeff.add : ∀ {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E]
  {f g : AddCircle T → E},
  MeasureTheory.Integrable f AddCircle.haarAddCircle →
    MeasureTheory.Integrable g AddCircle.haarAddCircle → fourierCoeff (f + g) = fourierCoeff f + fourierCoeff g
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.CasesEntry.mk.inj : ∀ {declName : Lean.Name} {eager : Bool} {declName_1 : Lean.Name} {eager_1 : Bool},
  { declName := declName, eager := eager } = { declName := declName_1, eager := eager_1 } →
    declName = declName_1 ∧ eager = eager_1
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.revAll_string_eq_revAll_toSlice : ∀ {pat : String} {s : String.Slice}, s.revAll pat = s.revAll pat.toSlice
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.complete : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], CauSeq.IsComplete ℤ_[p] norm
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.map_dblXYZ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).dblXYZ (⇑f ∘ P) = ⇑f ∘ W'.dblXYZ P
-- Init.Data.Array.Basic
Array.take_eq_extract : ∀ {α : Type u} {xs : Array α} {i : ℕ}, xs.take i = xs.extract 0 i
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.cancel_iso_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f f' : X ⟶ Y) (g : Y ≅ Z),
  CategoryTheory.CategoryStruct.comp f g.hom = CategoryTheory.CategoryStruct.comp f' g.hom ↔ f = f'
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instFree : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k], Module.Free k (SkewMonoidAlgebra k G)
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.coe_neg : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : NegZeroClass R] [inst_4 : ContinuousNeg R] (f : ContinuousMapZero X R), ⇑(-f) = -⇑f
-- Mathlib.Algebra.Order.Floor.Semifield
Mathlib.Meta.NormNum.IsNNRat.natFloor : ∀ {R : Type u_3} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (r : R) (n d : ℕ), Mathlib.Meta.NormNum.IsNNRat r n d → ∀ (res : ℕ), n / d = res → Mathlib.Meta.NormNum.IsNat ⌊r⌋₊ res
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.symm : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {v w : AbsoluteValue R S}, v.IsEquiv w → w.IsEquiv v
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
/-- An element of the fundamental group as an arrow in the fundamental groupoid.  -/
FundamentalGroup.toArrow : {X : Type u_1} → [inst : TopologicalSpace X] → {x : X} → FundamentalGroup X x → ({ as := x } ⟶ { as := x })
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.comp_smul : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y Z : C} {R : Type u_5} [inst_3 : Ring R]
  [inst_4 : CategoryTheory.Preadditive C] [inst_5 : CategoryTheory.Linear R C]
  [∀ (a : M), CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor C a)] (r : R) {a b c : M}
  (α : CategoryTheory.ShiftedHom X Y a) (β : CategoryTheory.ShiftedHom Y Z b) (h : b + a = c),
  α.comp (r • β) h = r • α.comp β h
-- Lean.Meta.AppBuilder
/-- Returns `@of_eq_true p h`  -/
Lean.Meta.mkOfEqTrueCore : Lean.Expr → Lean.Expr → Lean.Expr
-- Lean.Data.RArray
_private.Lean.Data.RArray.0.Lean.RArray.ofFn.go.eq_def : ∀ {α : Type u_1} {n : ℕ} (f : Fin n → α) (lb ub : ℕ) (h1 : lb < ub) (h2 : ub ≤ n),
  Lean.RArray.ofFn.go✝ f lb ub h1 h2 =
    if h : lb + 1 = ub then Lean.RArray.leaf (f ⟨lb, ⋯⟩)
    else
      let mid := (lb + ub) / 2;
      Lean.RArray.branch mid (Lean.RArray.ofFn.go✝ f lb mid ⋯ ⋯) (Lean.RArray.ofFn.go✝ f mid ub ⋯ h2)
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.hom_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : MvPolynomial τ R →+* S) (g : σ → MvPolynomial τ R) (φ : MvPolynomial σ R),
  f ((MvPolynomial.bind₁ g) φ) = (MvPolynomial.eval₂Hom (f.comp MvPolynomial.C) fun i => f (g i)) φ
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.le_le_combine_cert : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Bool
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.Measure.setIntegral_condKernel_univ_right : ∀ {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (β × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ] {E : Type u_3}
  {f : β × Ω → E} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace ℝ E] {s : Set β},
  MeasurableSet s →
    MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ρ →
      ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ
-- Mathlib.CategoryTheory.Subobject.Types
instWellPoweredType : CategoryTheory.WellPowered.{u, u, u + 1} (Type u)
-- Init.Control.Lawful.Instances
ExceptT.map_throw : ∀ {m : Type u_1 → Type u_2} {ε : Type u_1} [inst : Monad m] [LawfulMonad m] {α β : Type u_1} (f : α → β) (e : ε),
  f <$> throw e = throw e
-- Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure
/-- The Hahn–Jordan-based `totalVariation` agrees with the supremum-based `variation`.  -/
MeasureTheory.SignedMeasure.totalVariation_eq_variation : ∀ {X : Type u_1} {mX : MeasurableSpace X} (μ : MeasureTheory.SignedMeasure X),
  μ.totalVariation = MeasureTheory.VectorMeasure.variation μ
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray.go_eq : ∀ {α β : Type w} {m : Type w → Type w'} {it : Std.IterM m β} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [LawfulMonad m] [Std.Iterators.Finite α m] {acc : Array β},
  Std.IterM.toArray.go it acc = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => Std.IterM.toArray.go it' (acc.push out)
      | Std.IterStep.skip it' => Std.IterM.toArray.go it' acc
      | Std.IterStep.done => pure acc
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_toSubtype_subtype : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f ↑j)
      (CategoryTheory.Limits.biproduct.toSubtype f p) =
    CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) j
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.norm_starProjection_apply_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (v : E), ‖K.starProjection v‖ ≤ ‖v‖
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.ne_altitudeFoot : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.points i ≠ s.altitudeFoot i
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.comp_apply : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : Zero X] [inst_1 : Zero Y] [inst_2 : Zero R]
  [inst_3 : TopologicalSpace X] [inst_4 : TopologicalSpace Y] [inst_5 : TopologicalSpace R] (g : ContinuousMapZero Y R)
  (f : ContinuousMapZero X Y) (x : X), (g.comp f) x = g (f x)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coeFnMonoidHom_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Monoid β]
  [inst_3 : ContinuousMul β] (f : C(α, β)) (a : α), ContinuousMap.coeFnMonoidHom f a = f a
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.disjoint_of_disjoint_ae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  Disjoint (MeasureTheory.ae μ) (MeasureTheory.ae ν) → Disjoint μ ν
-- Mathlib.Analysis.Analytic.Within
/-- On open sets, `AnalyticOnNhd` and `AnalyticOn` coincide  -/
IsOpen.analyticOn_iff_analyticOnNhd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  IsOpen s → (AnalyticOn 𝕜 f s ↔ AnalyticOnNhd 𝕜 f s)
-- Mathlib.CategoryTheory.ComposableArrows.Four
/-- The morphism `mk₃ f₁ f₂₃ f₄ ⟶ mk₃ f₁₂ f₃ f₄` when `f₁ ≫ f₂ = f₁₂` and `f₂ ≫ f₂ = f₂₃`.  -/
CategoryTheory.ComposableArrows.fourδ₂Toδ₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {i₀ i₁ i₂ i₃ i₄ : C} →
      (f₁ : i₀ ⟶ i₁) →
        (f₂ : i₁ ⟶ i₂) →
          (f₃ : i₂ ⟶ i₃) →
            (f₄ : i₃ ⟶ i₄) →
              (f₁₂ : i₀ ⟶ i₂) →
                (f₂₃ : i₁ ⟶ i₃) →
                  autoParam (CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
                      CategoryTheory.ComposableArrows.fourδ₂Toδ₁._auto_1 →
                    autoParam (CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃)
                        CategoryTheory.ComposableArrows.fourδ₂Toδ₁._auto_3 →
                      (CategoryTheory.ComposableArrows.mk₃ f₁ f₂₃ f₄ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁₂ f₃ f₄)
-- Mathlib.Logic.Equiv.Prod
Equiv.curry_symm_apply : ∀ (α : Type u_9) (β : Type u_10) (γ : Sort u_11), ⇑(Equiv.curry α β γ).symm = Function.uncurry
-- Mathlib.Topology.Constructions
ContinuousAt.finCons : ∀ {X : Type u} [inst : TopologicalSpace X] {n : ℕ} {A : Fin (n + 1) → Type u_9}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)] {f : X → A 0} {g : X → (j : Fin n) → A j.succ} {x : X},
  ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun a => Fin.cons (f a) (g a)) x
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.identities_of_prop₂_of_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} {f : X ⟶ Y},
  W₂ f → r.deg X = r.deg Y → CategoryTheory.MorphismProperty.identities C f
-- Init.Data.Nat.Basic
Nat.or_exists_add_one : ∀ {p : ℕ → Prop}, (p 0 ∨ ∃ n, p (n + 1)) ↔ Exists p
-- Lean.Util.PtrSet
Lean.PtrMap.find? : {α β : Type} → Lean.PtrMap α β → α → Option β