mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Lemmas
List.splitAt.go.eq_2 : ∀ {α : Type u} (l a : List α) (x_3 : α) (xs : List α) (n : ℕ),
  List.splitAt.go l (x_3 :: xs) n.succ a = List.splitAt.go l xs n (x_3 :: a)
-- Mathlib.Data.Nat.MaxPowDiv
/-- **Alias** of `padicValNat_zero_right`. -/
Nat.maxPowDiv.zero : ∀ (p : ℕ), padicValNat p 0 = 0
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
/-- Maps into the zero module are trivial  -/
QuadraticMap.Isometry.instSubsingleton : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} [Subsingleton M₂],
  Subsingleton (Q₁ →qᵢ Q₂)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The isomorphism `(γ → α × β) ≃ (γ → α) × (γ → β)` as a measurable equivalence.  -/
MeasurableEquiv.arrowProdEquivProdArrow : (α : Type u_8) →
  (β : Type u_9) →
    (γ : Type u_10) → [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → (γ → α × β) ≃ᵐ (γ → α) × (γ → β)
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The cycles of the short complex `shortComplex` at `E^{n₁}(f₁, f₂, f₃)`
identifies to `Z^{n₁}(f₁, f₂)`.  -/
CategoryTheory.Abelian.SpectralObject.cyclesIso : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (n₀ n₁ n₂ : ℤ) →
                      (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesIso._auto_1) →
                        (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cyclesIso._auto_3) →
                          (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).cycles ≅ X.cycles f₁ f₂ n₁
-- Mathlib.Topology.Separation.Basic
instLocallyCompactPairOfWeaklyLocallyCompactSpaceOfR1Space : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] [inst_2 : TopologicalSpace Y]
  [R1Space Y], LocallyCompactPair X Y
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.normalize : ∀ {x y z : ℤ}, PythagoreanTriple x y z → PythagoreanTriple (x / ↑(x.gcd y)) (y / ↑(x.gcd y)) (z / ↑(x.gcd y))
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDecl.mk : Lean.Name → Array Lean.Meta.SimpTheoremKey → Lean.Meta.Simp.SimprocDecl
-- Mathlib.Algebra.Notation.Prod
Prod.instAdd.eq_1 : ∀ {M : Type u_8} {N : Type u_9} [inst : Add M] [inst_1 : Add N],
  Prod.instAdd = { add := fun p q => (p.1 + q.1, p.2 + q.2) }
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.uncurry_curry : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y : C}
  [inst_2 : CategoryTheory.Closed A] (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A X ⟶ Y),
  CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.MonoidalClosed.curry f) = f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β] {f : β → β}, (t.modify k f)[k]! = (Option.map f t[k]?).get!
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.profiniteCompletion_obj : ∀ (G : GrpCat), ProfiniteGrp.profiniteCompletion.obj G = ProfiniteGrp.ProfiniteCompletion.completion G
-- Init.Data.List.Scan.Lemmas
List.scanrM_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [inst : Monad m] [LawfulMonad m] {f : α → β → β}
  {as : List α}, List.scanrM (fun x1 x2 => pure (f x1 x2)) init as = pure (List.scanr f init as)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Reindex a wide pullback cone.  -/
CategoryTheory.Limits.WidePullbackCone.reindex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_2} →
      {X : C} →
        {Y : ι → C} →
          {f : (i : ι) → Y i ⟶ X} →
            CategoryTheory.Limits.WidePullbackCone f →
              {ι' : Type u_3} → (e : ι' ≃ ι) → CategoryTheory.Limits.WidePullbackCone fun i => f (e i)
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
/-- The box `{0, ..., d - 1}^n` as a `Finset`.  -/
Behrend.box : (n : ℕ) → ℕ → Finset (Fin n → ℕ)
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.inv_apply : ∀ (α : Type u) [inst : Group α] [inst_1 : LE α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α] (a : α),
  (OrderIso.inv α) a = OrderDual.toDual a⁻¹
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.fiberHomeo_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (y : ↥Y) (x : ↥(AlgebraicGeometry.Scheme.Hom.fiber f y)),
  ↑((AlgebraicGeometry.Scheme.Hom.fiberHomeo f y) x) = (AlgebraicGeometry.Scheme.Hom.fiberι f y) x
-- Batteries.Data.Fin.Lemmas
Fin.exists_minimal_of_findSome?_eq_some : ∀ {n : ℕ} {α : Type u_1} {x : α} {f : Fin n → Option α},
  Fin.findSome? f = some x → ∃ i, f i = some x ∧ ∀ j < i, f j = none
-- Mathlib.Order.Circular
sbtw_irrefl : ∀ {α : Type u_1} [inst : CircularPreorder α] (a : α), ¬sbtw a a a
-- Mathlib.Algebra.Ring.Pi
/-- Evaluation of functions into an indexed collection of non-unital rings at a point is a
non-unital ring homomorphism. This is `Function.eval` as a `NonUnitalRingHom`.  -/
Pi.evalNonUnitalRingHom : {I : Type u} →
  (f : I → Type v) → [inst : (i : I) → NonUnitalNonAssocSemiring (f i)] → (i : I) → ((i : I) → f i) →ₙ+* f i
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
/-- If `G` preserves binary coproducts and `C` has them, then the binary cofan constructed of the mapped
morphisms of the binary product cocone is a colimit.
 -/
CategoryTheory.Limits.isColimitOfHasBinaryCoproductOfPreservesColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          (X Y : C) →
            [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y] →
              [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) G] →
                CategoryTheory.Limits.IsColimit
                  (CategoryTheory.Limits.BinaryCofan.mk (G.map CategoryTheory.Limits.coprod.inl)
                    (G.map CategoryTheory.Limits.coprod.inr))
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.lt_norm_expr_nc : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [Lean.Grind.OrderedRing α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs lhs' rhs' : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.norm_cnstr_nc_cert lhs rhs lhs' rhs' = true →
    (Lean.Grind.CommRing.Expr.denote ctx lhs < Lean.Grind.CommRing.Expr.denote ctx rhs) =
      (Lean.Grind.CommRing.Expr.denote ctx lhs' < Lean.Grind.CommRing.Expr.denote ctx rhs')
-- Mathlib.Data.Rat.Init
Rat.instNNRatCast : NNRatCast ℚ
-- Std.Internal.UV.System
/-- Gets the parent process ID of the current process.
 -/
Std.Internal.UV.System.osGetPpid : IO UInt64
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_eq_get!_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α}, Std.ExtDTreeMap.Const.get! t a = (Std.ExtDTreeMap.Const.get? t a).get!
-- Mathlib.Data.Nat.Cast.Order.Ring
/-- See also `Nat.ofNat_pos`, specialised to `IsOrderedRing`.  -/
Nat.ofNat_pos' : ∀ {α : Type u_2} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [NeZero 1]
  {n : ℕ} [inst_5 : n.AtLeastTwo], 0 < OfNat.ofNat n
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.Normal.map_addConj_eq : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [H.Normal] (g : G), AddSubgroup.map (↑(AddAut.addConj g)) H = H
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.SigmaFinite.of_isFiniteMeasureOnCompacts : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] [SigmaCompactSpace α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasureOnCompacts μ], MeasureTheory.SigmaFinite μ
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.mk'.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M ≃ N) (h : ∀ (x y : M), f (x + y) = f x + f y),
  AddEquiv.mk' f h = { toEquiv := f, map_add' := h }
-- Mathlib.Data.Bool.Basic
Bool.eq_true_of_not_eq_false' : ∀ {a : Bool}, (!a) = false → a = true
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringRightObjCompIso_inv_app_app : ∀ {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] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D')
  (X : CategoryTheory.Functor E C) (X_1 : E),
  ((F.whiskeringRightObjCompIso G).inv.app X).app X_1 = CategoryTheory.CategoryStruct.id (G.obj (F.obj (X.obj X_1)))
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
/-- The bijection `I.sections ≃ I.multicospan.sections` when `I : MulticospanIndex (Type u)`
is a multiequalizer diagram in the category of types.  -/
CategoryTheory.Limits.MulticospanIndex.sectionsEquiv : {J : CategoryTheory.Limits.MulticospanShape} →
  (I : CategoryTheory.Limits.MulticospanIndex J (Type u)) → I.sections ≃ ↑I.multicospan.sections
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.mk_eq_zero_iff : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (x : ↥P.ker), Algebra.Extension.Cotangent.mk x = 0 ↔ ↑x ∈ P.ker ^ 2
-- Mathlib.Algebra.Group.ULift
ULift.cancelCommMonoid.eq_1 : ∀ {α : Type u} [inst : CancelCommMonoid α],
  ULift.cancelCommMonoid = Function.Injective.cancelCommMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Functions.apply₁.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (f : L.Functions 1) (t : L.Term α),
  f.apply₁ t = FirstOrder.Language.func f ![t]
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.cancelDen : Lean.Meta.Grind.Arith.Linear.RingEqCnstr →
  ℤ → Lean.Grind.Linarith.Var → Lean.Grind.Linarith.Var → Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Mul-div-div version.  -/
Finset.ruzsa_triangle_inequality_mul_div_div : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : CommGroup G] (A B C : Finset G),
  (A * C).card * B.card ≤ (A / B).card * (B / C).card
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.length_empty : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R), f.length ∅ = 0
-- Init.Data.List.TakeDrop
List.lt_length_of_take_ne_self : ∀ {α : Type u_1} {l : List α} {i : ℕ}, List.take i l ≠ l → i < l.length
-- Std.Internal.UV.System
Std.Internal.UV.System.instInhabitedRUsage : Inhabited Std.Internal.UV.System.RUsage
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImportMetaKind.nonMeta.sizeOf_spec : sizeOf Lean.Lsp.LeanImportMetaKind.nonMeta = 1
-- Mathlib.Data.TypeVec
/-- cases distinction for an arrow in the category of (n+1)-length type vectors  -/
TypeVec.typevecCasesCons₃ : (n : ℕ) →
  {β : (v : TypeVec.{u_2} (n + 1)) → (v' : TypeVec.{u_3} (n + 1)) → v.Arrow v' → Sort u_1} →
    ((t : Type u_2) →
        (t' : Type u_3) →
          (f : t → t') →
            (v : TypeVec.{u_2} n) → (v' : TypeVec.{u_3} n) → (fs : v.Arrow v') → β (v ::: t) (v' ::: t') (fs ::: f)) →
      (v : TypeVec.{u_2} (n + 1)) → (v' : TypeVec.{u_3} (n + 1)) → (fs : v.Arrow v') → β v v' fs
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ ∩ t₂).getKey? k = t₁.getKey? k
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.impIff : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (t : CategoryTheory.Limits.IsInitial X),
  (CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial t).inv = 0
-- Lean.Elab.InfoTree.Basic
/-- Adds the given trailing substring to all adjacent syntax in the info tree if any, otherwise returns
`none`.
 -/
Lean.Elab.InfoTree.addTrailing? : Substring.Raw → Lean.Elab.InfoTree → Option Lean.Elab.InfoTree
-- Mathlib.Data.List.Map2
List.map₂Right_nil_right : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (as : List α), List.map₂Right f as [] = []
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A point is in the `affineSpan` of an indexed family if and only
if it is an `affineCombination` with sum of weights 1, provided the
underlying ring is nontrivial.  -/
mem_affineSpan_iff_eq_affineCombination : ∀ {ι : Type u_1} (k : Type u_2) (V : Type u_3) {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [Nontrivial k] {p1 : P} {p : ι → P},
  p1 ∈ affineSpan k (Set.range p) ↔ ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insert k v).isEmpty = false
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.sum_biUnion_boxes : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {M : Type u_2} [inst : AddCommMonoid M] (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (f : BoxIntegral.Box ι → M),
  ∑ J ∈ π.boxes.biUnion fun J => (πi J).boxes, f J = ∑ J ∈ π.boxes, ∑ J' ∈ (πi J).boxes, f J'
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.inv_smul_integral_comp_div_add : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (c d : ℝ),
  c⁻¹ • ∫ (x : ℝ) in a..b, f (x / c + d) = ∫ (x : ℝ) in a / c + d..b / c + d, f x
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.toSmoothPartitionOfUnity_eq_mul_prod : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s)
  [inst_6 : T2Space M] [inst_7 : IsManifold I (↑⊤) M] (i : ι) (x : M) (t : Finset ι),
  (∀ (j : ι), WellOrderingRel j i → ↑(fs.toFun j) x ≠ 0 → j ∈ t) →
    (fs.toSmoothPartitionOfUnity i) x = ↑(fs.toFun i) x * ∏ j ∈ t with WellOrderingRel j i, (1 - ↑(fs.toFun j) x)
-- Lean.Elab.App
/-- Process a `fType` of the form `(x : A) → B x`.
This method assume `fType` is a function type.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.processExplicitArg : Lean.Name → Lean.Elab.Term.ElabAppArgs.M Lean.Expr
-- Mathlib.Data.NNReal.Defs
/-- Nonnegative real numbers, denoted as `ℝ≥0` within the NNReal namespace  -/
NNReal : Type
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Morphisms for `WithTerminal C`.  -/
CategoryTheory.WithTerminal.Hom : {C : Type u} →
  [CategoryTheory.Category.{v, u} C] → CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → Type v
-- Mathlib.Data.Set.Basic
/-- **Alias** of the forward direction of `Set.univ_subset_iff`. -/
Set.eq_univ_of_univ_subset : ∀ {α : Type u} {s : Set α}, Set.univ ⊆ s → s = Set.univ
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.splitOn.loop : Substring.Raw → String → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw → List Substring.Raw → List Substring.Raw
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.δ_map_assoc : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex (n + 1) x) (i : Fin (n + 2)) {Z : SSet}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i) (CategoryTheory.CategoryStruct.comp f.map h) =
    CategoryTheory.CategoryStruct.comp (SSet.const x) h
-- Init.Conv
/-- `cbv` performs simplification that closely mimics call-by-value evaluation.
It reduces the target term by unfolding definitions using their defining equations and
applying matcher equations. The unfolding is propositional, so `cbv` also works
with functions defined via well-founded recursion or partial fixpoints.

The proofs produced by `cbv` only use the three standard axioms.
In particular, they do not require trust in the correctness of the code
generator.
 -/
Lean.Parser.Tactic.Conv.cbv : Lean.ParserDescr
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.mkJoinPoint : Lean.Name → Array (Lean.Syntax × Bool) → Lean.Syntax → Lean.Syntax → Lean.Elab.Term.Do.ToTerm.M Lean.Syntax
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.pullback_def : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : NormedAddCommGroup E] (f : CompactlySupportedContinuousMap B E) (b : B) (a : A),
  (H.pullback f b) a = f (b * φ a)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The state transition function.  -/
Turing.TM1.step : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      [inst : Inhabited Γ] → (Λ → Turing.TM1.Stmt Γ Λ σ) → Turing.TM1.Cfg Γ Λ σ → Option (Turing.TM1.Cfg Γ Λ σ)
-- Mathlib.Order.Filter.Pointwise
Filter.vaddCommClass_filter' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α γ] [inst_1 : VAdd β γ] [VAddCommClass α β γ],
  VAddCommClass α (Filter β) (Filter γ)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.bijective : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), Function.Bijective ⇑e
-- Init.Data.ByteArray.Basic
/-- Moves the iterator's position forward by one byte, unconditionally.

It is only valid to call this function if the iterator is not at the end of the array, **i.e.**
`Iterator.atEnd` is `false`; otherwise, the resulting iterator will be invalid.
 -/
ByteArray.Iterator.next : ByteArray.Iterator → ByteArray.Iterator
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateLetDeclCoreImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetDecl pu → Lean.Expr → Lean.Compiler.LCNF.LetValue pu → Lean.Compiler.LCNF.LetDecl pu
-- Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
homeomorphSphereProd_apply_snd_coe : ∀ (E : Type u_2) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (r : ℝ) (hr : 0 < r) (x : ↑{0}ᶜ),
  ↑((homeomorphSphereProd E r hr) x).2 = ‖↑x‖ / r
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- Semilinear sets are closed under union.  -/
IsSemilinearSet.union : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s₁ s₂ : Set M},
  IsSemilinearSet s₁ → IsSemilinearSet s₂ → IsSemilinearSet (s₁ ∪ s₂)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- One can reformulate smoothness as continuity and smoothness in any extended chart.  -/
mdifferentiable_iff : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} [IsManifold I 1 M]
  [IsManifold I' 1 M'],
  MDiff f ↔
    Continuous f ∧
      ∀ (x : M) (y : M'),
        DifferentiableOn 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' f ⁻¹' (extChartAt I' y).source)
-- Mathlib.Algebra.Jordan.Basic
commute_rmul_rmul_sq : ∀ {A : Type u_1} [inst : NonUnitalNonAssocRing A] [IsJordan A] (a : A),
  Commute (AddMonoid.End.mulRight a) (AddMonoid.End.mulRight (a * a))
-- Lean.Declaration
Lean.QuotKind.type : Lean.QuotKind
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- The result of normalizing a 1-morphism.  -/
Mathlib.Tactic.BicategoryLike.Normalize.Result : Type
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
/-- Converting a homogeneous ideal to an ideal.  -/
HomogeneousIdeal.toIdeal : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubmonoidClass σ A] →
            {𝒜 : ι → σ} →
              [inst_3 : DecidableEq ι] → [inst_4 : AddMonoid ι] → [inst_5 : GradedRing 𝒜] → HomogeneousIdeal 𝒜 → Ideal A
-- Mathlib.Order.Filter.EventuallyConst
Filter.eventuallyConst_set' : ∀ {α : Type u_1} {l : Filter α} {s : Set α}, Filter.EventuallyConst s l ↔ s =ᶠ[l] ∅ ∨ s =ᶠ[l] Set.univ
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ℚ → ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ (a : α) {A : Set β}, MeasurableSet A → ∀ (q : ℚ), ∫ (c : β) in A, f (a, c) q ∂ν a = (κ a).real (A ×ˢ Set.Iic ↑q)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedResponse.default : {α : Type u} → [Inhabited α] → Lean.JsonRpc.Response α
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
_private.Mathlib.SetTheory.Ordinal.CantorNormalForm.0.Ordinal.CNF.rec.eq_1 : ∀ (b : Ordinal.{u_2}) {C : Ordinal.{u_2} → Sort u_1} (H0 : C 0)
  (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ Ordinal.log b o) → C o) (o : Ordinal.{u_2}),
  Ordinal.CNF.rec b H0 H o = if h : o = 0 then ⋯ ▸ H0 else H o h (Ordinal.CNF.rec b H0 H (o % b ^ Ordinal.log b o))
-- Lean.Server.ServerTask
Lean.Server.ServerTask.cancel : {α : Type u_1} → Lean.Server.ServerTask α → BaseIO Unit
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Equiv.multipliable_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  (e : γ ≃ β), Multipliable (f ∘ ⇑e) ↔ Multipliable f
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- If the angle between two vectors is π, the angles between those
vectors and a third vector add to π.  -/
InnerProductGeometry.angle_add_angle_eq_pi_of_angle_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V} (z : V),
  InnerProductGeometry.angle x y = Real.pi → InnerProductGeometry.angle x z + InnerProductGeometry.angle y z = Real.pi
-- Mathlib.Util.Notation3
Mathlib.Notation3.DelabKey.app.injEq : ∀ (const : Option Lean.Name) (arity : ℕ) (const_1 : Option Lean.Name) (arity_1 : ℕ),
  (Mathlib.Notation3.DelabKey.app const arity = Mathlib.Notation3.DelabKey.app const_1 arity_1) =
    (const = const_1 ∧ arity = arity_1)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLE_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α fun x => β}
  (hto : t.Ordered) {k : α} (he : ∃ a ∈ t, (compare a k).isLE = true),
  Std.DTreeMap.Internal.Impl.Const.getEntryLE k t hto he =
    ((Std.DTreeMap.Internal.Impl.getEntryLE k t hto he).fst, (Std.DTreeMap.Internal.Impl.getEntryLE k t hto he).snd)