mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Semicontinuity.Defs
upperHemicontinuousWithinAt_univ_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α},
  UpperHemicontinuousWithinAt f Set.univ x ↔ UpperHemicontinuousAt f x
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.simp.rfl.checkTransparency : Lean.Option Bool
-- Mathlib.Algebra.Group.Defs
/-- `ZPow` is an implementation detail of `DivInvMonoid`. It is needed because it is
impossible to extend `Pow M ℕ` and `Pow M ℤ` at the same time.  -/
ZPow : Type u → Type u
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
ContMDiff.comp_contMDiffOn : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] {E'' : Type u_8} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E'']
  {H'' : Type u_9} [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10}
  [inst_12 : TopologicalSpace M''] [inst_13 : ChartedSpace H M] [inst_14 : ChartedSpace H' M']
  [inst_15 : ChartedSpace H'' M''] {n : WithTop ℕ∞} {f : M → M'} {g : M' → M''} {s : Set M},
  ContMDiff I' I'' n g → ContMDiffOn I I' n f s → ContMDiffOn I I'' n (g ∘ f) s
-- Mathlib.Order.Minimal
OrderEmbedding.maximal_apply_mem_iff : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {f : α ↪o β} {t : Set β},
  t ⊆ Set.range ⇑f → (Maximal (fun x => x ∈ t) (f x) ↔ Maximal (fun x => f x ∈ t) x)
-- Std.Tactic.Do.Syntax
/-- `mexfalso` is like `exfalso`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P : SPred σs) : ⌜False⌝ ⊢ₛ P := by
  mintro HP
  mexfalso
  mexact HP
```
 -/
Lean.Parser.Tactic.mexfalso : Lean.ParserDescr
-- Init.Data.List.SplitOn.Basic
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPPrepend.eq_2 : ∀ {α : Type u_1} (p : α → Bool) (x : List α) (a : α) (t : List α),
  List.splitOnPPrepend p (a :: t) x =
    if p a = true then x.reverse :: List.splitOnPPrepend p t [] else List.splitOnPPrepend p t (a :: x)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.lt_of_lt_of_le : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a b c : α},
  Std.PRange.UpwardEnumerable.LT a b → Std.PRange.UpwardEnumerable.LE b c → Std.PRange.UpwardEnumerable.LT a c
-- Batteries.Data.Random.MersenneTwister
/-- Mersenne Twister iteration.  -/
Batteries.Random.MersenneTwister.State.next : {cfg : Batteries.Random.MersenneTwister.Config} →
  Batteries.Random.MersenneTwister.State cfg → BitVec cfg.wordSize × Batteries.Random.MersenneTwister.State cfg
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.mul_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f₁ f₂ : ι → α} {g : ι → β},
  MonovaryOn f₁ g s → MonovaryOn f₂ g s → MonovaryOn (f₁ * f₂) g s
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Equiv.prodSubtypeFstEquivSubtypeProd.eq_1 : ∀ {α : Type u_9} {β : Type u_10} {p : α → Prop},
  Equiv.prodSubtypeFstEquivSubtypeProd =
    { toFun := fun x => (⟨(↑x).1, ⋯⟩, (↑x).2), invFun := fun x => ⟨(↑x.1, x.2), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Field.Opposite
MulOpposite.op_nnratCast : ∀ {α : Type u_1} [inst : NNRatCast α] (q : ℚ≥0), MulOpposite.op ↑q = ↑q
-- Lean.Meta.WHNF
Lean.Meta.reduceBinNatOp : (ℕ → ℕ → ℕ) → Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Data.Rat.Defs
Rat.pow_eq_mkRat : ∀ (q : ℚ) (n : ℕ), q ^ n = mkRat (q.num ^ n) (q.den ^ n)
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
/-- The tangent bundle of a product is canonically isomorphic to the product of the tangent
bundles.  -/
equivTangentBundleProd : {𝕜 : 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'] →
                                        TangentBundle (I.prod I') (M × M') ≃ TangentBundle I M × TangentBundle I' M'
-- Mathlib.Tactic.Widget.StringDiagram
/-- The list of nodes associated with a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.nodes : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    Mathlib.Tactic.BicategoryLike.NormalExpr →
      Mathlib.Tactic.BicategoryLike.CoherenceM ρ (List (List Mathlib.Tactic.Widget.StringDiagram.Node))
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.instFinitePresentationModelOfHasCoeffsOfFinite : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀] [Finite ι]
  [Finite σ], Algebra.FinitePresentation R₀ (Algebra.Presentation.ModelOfHasCoeffs R₀)
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- A point in the mulAntidiagonal is determined by its first coordinate.

See also `Finset.mulAntidiagonal_congr'`.  -/
Finset.HasMulAntidiagonal.mulAntidiagonal_congr : ∀ {A : Type u_1} [inst : CancelMonoid A] [inst_1 : Finset.HasMulAntidiagonal A] {p q : A × A} {n : A},
  p ∈ Finset.HasMulAntidiagonal.mulAntidiagonal n →
    q ∈ Finset.HasMulAntidiagonal.mulAntidiagonal n → (p = q ↔ p.1 = q.1)
-- Mathlib.Control.Random
/-- `Random m α` gives us machinery to generate values of type `α` in the monad `m`.

Note that `m` is a parameter as some types may only be sampleable with access to a certain monad.  -/
Random : (Type u → Type u_1) → Type u → Type (max (max 1 u) u_1)
-- Mathlib.Topology.Gluing
TopCat.GlueData.fromOpenSubsetsGlue_injective : ∀ {α : Type u} [inst : TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α),
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.GlueData.fromOpenSubsetsGlue U))
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_mulEquiv_trans : ∀ {R : Type u_4} {S : Type u_5} {S' : Type u_6} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S]
  [inst_4 : Mul S'] [inst_5 : Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S'), ↑(e₁.trans e₂) = (↑e₁).trans ↑e₂
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.rightUnitor_inv_app : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  (F : CategoryTheory.Functor J C) (j : J),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor F).inv.app j =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj j)).inv
-- Mathlib.Combinatorics.Quiver.SingleObj
/-- Auxiliary definition for `quiver.SingleObj.pathEquivList`.
Converts a list of elements of type `α` into a path in the quiver `SingleObj α`.
 -/
Quiver.SingleObj.listToPath : {α : Type u_1} → List α → Quiver.Path (Quiver.SingleObj.star α) (Quiver.SingleObj.star α)
-- Lean.DocString.Markdown
/-- Builtin block renderers, for bootstrapping.  -/
_private.Lean.DocString.Markdown.0.Lean.Doc.builtinBlockMdRenderers : IO.Ref (Lean.NameMap Lean.Doc.BlockMdRenderer)
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- A point on a line through a point on a sphere equals that point or `secondInter`.  -/
EuclideanGeometry.Sphere.eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P},
  p ∈ s → ∀ {v : V} {p' : P}, p' ∈ AffineSubspace.mk' p (ℝ ∙ v) → (p' = p ∨ p' = s.secondInter p v ↔ p' ∈ s)
-- Mathlib.Tactic.Ring.Compare
Mathlib.Tactic.Ring.le_congr : ∀ {α : Type u_1} [inst : LE α] {a b c d : α}, a = b → b ≤ c → d = c → a ≤ d
-- Mathlib.Order.Basic
Prod.lt_of_lt_of_le : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {x y : α × β}, x.1 < y.1 → x.2 ≤ y.2 → x < y
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.instHasPullback : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.HasPullback f g
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorem.mk : Array Lean.Meta.SimpTheoremKey →
  Array Lean.Name → Lean.Expr → ℕ → Bool → Bool → Lean.Meta.Origin → Bool → Bool → Lean.Meta.SimpTheorem
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited γ] {f : α → β → Option γ} {k : α},
  (Std.ExtHashMap.filterMap f m)[k]! = (m[k]?.pbind fun x_2 h' => f (m.getKey k ⋯) x_2).get!
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.sub_comp : ∀ {R : Type u} [inst : Ring R] {p q r : Polynomial R}, (p - q).comp r = p.comp r - q.comp r
-- Mathlib.Tactic.Rename
/-- A parser for a single rename to perform in the `rename` tactic:
these should have the form `h => hnew` (describing a rename of a hypothesis `h` to `hnew`).  -/
Mathlib.Tactic.renameArg : Lean.ParserDescr
-- Mathlib.Order.Category.Lat
Lat.forget_map : ∀ {X Y : Lat} (f : X ⟶ Y),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget Lat).map f)) = ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.defn : {γ : Type} → Lean.KeyedDeclsAttribute γ → Lean.KeyedDeclsAttribute.Def γ
-- Std.Sync.Barrier
_private.Std.Sync.Barrier.0.Std.Barrier.mk.injEq : ∀ (lock : Std.Mutex Std.BarrierState✝) (cvar : Std.Condvar) (numThreads : ℕ) (lock_1 : Std.Mutex Std.BarrierState✝)
  (cvar_1 : Std.Condvar) (numThreads_1 : ℕ),
  ({ lock := lock, cvar := cvar, numThreads := numThreads } =
      { lock := lock_1, cvar := cvar_1, numThreads := numThreads_1 }) =
    (lock = lock_1 ∧ cvar = cvar_1 ∧ numThreads = numThreads_1)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- Given any point `x` and `f` in the homogeneous localization at `x`, there is an element in the
stalk at `x` obtained by `sectionInBasicOpen`. This is the inverse of `stalkToFiberRingHom`.
 -/
AlgebraicGeometry.homogeneousLocalizationToStalk : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (x : ↑(ProjectiveSpectrum.top 𝒜)) →
                HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal →
                  ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.stalk x)
-- Init.Data.Nat.Gcd
Nat.gcd_pos_of_pos_right : ∀ (m : ℕ) {n : ℕ}, 0 < n → 0 < m.gcd n
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The right fraction corresponding to a left fraction in the opposite category.  -/
CategoryTheory.MorphismProperty.LeftFraction.unop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty Cᵒᵖ} →
      {X Y : Cᵒᵖ} → W.LeftFraction X Y → W.unop.RightFraction (Opposite.unop Y) (Opposite.unop X)
-- Mathlib.Analysis.Normed.Group.Hom
/-- The group homomorphism underlying a bounded group homomorphism.  -/
NormedAddGroupHom.toAddMonoidHom : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → NormedAddGroupHom V₁ V₂ → V₁ →+ V₂
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l →
      k ∈ l → ∀ {h : k' ∈ Std.ExtHashSet.ofList l}, (Std.ExtHashSet.ofList l).get k' h = k
-- Lean.Environment
/-- Returns the data saved by `ext.exportEntriesFn` when `m` was elaborated. See docs on the function for
details. When using the module system, `level` can be used to select the level of data to retrieve,
but is limited to the maximum level actually imported: `exported` on the cmdline and `server` in the
language server. Higher levels will return the data of the maximum imported level.
 -/
Lean.PersistentEnvExtension.getModuleEntries : {α β σ : Type} →
  [Inhabited σ] →
    Lean.PersistentEnvExtension α β σ →
      Lean.Environment → Lean.ModuleIdx → optParam Lean.OLeanLevel Lean.OLeanLevel.exported → Array α
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_eq_metric : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) {x : E} {r : ℝ}, p.closedBall x r = Metric.closedBall x r
-- Mathlib.RingTheory.Congruence.BigOperators
/-- Congruence relation of a ring preserves finite sum indexed by a list.  -/
RingCon.listSum : ∀ {ι : Type u_1} {S : Type u_2} [inst : AddMonoid S] [inst_1 : Mul S] (t : RingCon S) (l : List ι) {f g : ι → S},
  (∀ i ∈ l, t (f i) (g i)) → t (List.map f l).sum (List.map g l).sum
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_eq_false_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.contains a = true → t.isEmpty = false
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup'_neg : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Neg α] [inst_2 : SemilatticeSup β] {s : Finset α}
  (hs : (-s).Nonempty) (f : α → β), (-s).sup' hs f = s.sup' ⋯ fun x => f (-x)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ring.inj : ∀ {c : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr} {lhs : Lean.Meta.Grind.Arith.Linear.LinExpr}
  {c_1 : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr} {lhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr},
  Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ring c lhs = Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ring c_1 lhs_1 →
    c = c_1 ∧ lhs = lhs_1
-- Mathlib.MeasureTheory.Function.JacobianOneDim
/-- Change of variable formula for differentiable functions: if a real function `f` is
monotone and differentiable on a measurable set `s`, then the Lebesgue integral of a function
`u : ℝ → ℝ≥0∞` on `f '' s` coincides with the integral of `(f' x) * u ∘ f` on `s`.
Note that the measurability of `f '' s` is given by `MeasurableSet.image_of_monotoneOn`.  -/
MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn : ∀ {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
      MonotoneOn f s → ∀ (u : ℝ → ENNReal), ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Right.one_lt_mul_of_right`. -/
one_lt_mul_of_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [IsBotOneClass α] [MulRightMono α] {b : α},
  1 < b → ∀ (a : α), 1 < a * b
-- Mathlib.AlgebraicGeometry.Fiber
/-- The fiber of `f` at `y` is naturally a `κ(y)`-scheme.  -/
AlgebraicGeometry.Scheme.Hom.fiberOverSpecResidueField : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) → (y : ↥Y) → (AlgebraicGeometry.Scheme.Hom.fiber f y).Over (AlgebraicGeometry.Spec (Y.residueField y))
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- **Constructive Church-Rosser theorem** (compare `FreeGroup.Red.church_rosser`).  -/
FreeGroup.reduce.churchRosser : {α : Type u_1} →
  {L₁ L₂ L₃ : List (α × Bool)} →
    [DecidableEq α] → FreeGroup.Red L₁ L₂ → FreeGroup.Red L₁ L₃ → { L₄ // FreeGroup.Red L₂ L₄ ∧ FreeGroup.Red L₃ L₄ }
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
/-- The equivalence `(C ⥤ D) ≌ (Karoubi C ⥤ D)` when `D` is idempotent complete.  -/
CategoryTheory.Idempotents.karoubiUniversal : (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] →
        [CategoryTheory.IsIdempotentComplete D] →
          CategoryTheory.Functor C D ≌ CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) D
-- Init.Data.Option.Attach
Option.unattach_filter : ∀ {α : Type u_1} {p : α → Prop} {o : Option { x // p x }} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → (Option.filter f o).unattach = Option.filter g o.unattach
-- Init.SizeOf
Lean.Syntax.SepArray.mk.sizeOf_spec : ∀ {sep : String} (elemsAndSeps : Array Lean.Syntax), sizeOf { elemsAndSeps := elemsAndSeps } = 1 + sizeOf elemsAndSeps
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.denom_cocycle_σ : ∀ (g h : GL (Fin 2) ℝ) (z : UpperHalfPlane),
  UpperHalfPlane.denom (g * h) ↑z = (UpperHalfPlane.σ h) (UpperHalfPlane.denom g ↑(h • z)) * UpperHalfPlane.denom h ↑z
-- Mathlib.Algebra.Homology.LeftResolution.Basic
/-- The morphism `Λ.chainComplex X ⟶ Λ.chainComplex Y` of chain complexes
induced by `f : X ⟶ Y`.  -/
CategoryTheory.Abelian.LeftResolution.chainComplexMap : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} →
          (Λ : CategoryTheory.Abelian.LeftResolution ι) →
            {X Y : A} →
              (X ⟶ Y) →
                [inst_2 : ι.Full] →
                  [inst_3 : ι.Faithful] →
                    [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] →
                      [inst_5 : CategoryTheory.Abelian A] → Λ.chainComplex X ⟶ Λ.chainComplex Y
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.ofAIG.eq_1 : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (aig : Std.Sat.AIG α),
  Std.Sat.AIG.RelabelNat.State.ofAIG aig = (Std.Sat.AIG.RelabelNat.State.ofAIGAux aig).map
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.decidableLT : {α : Type u_1} →
  [inst : CommMonoid α] →
    [inst_1 : PartialOrder α] →
      [inst_2 : IsOrderedCancelMonoid α] → {s : Submonoid α} → [DecidableLT α] → DecidableLT (Localization s)
-- Mathlib.Logic.Function.Basic
Function.instIsEquivOnFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [IsEquiv β r], IsEquiv α (Function.onFun r f)
-- Mathlib.Topology.Neighborhoods
/-- Suppose that `f` sends the complement to `s` to a single point `x`, and `l` is some filter.
Then `f` tends to `x` along `l` restricted to `s` if and only if it tends to `x` along `l`.  -/
tendsto_inf_principal_nhds_iff_of_forall_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {f : α → X} {l : Filter α} {s : Set α},
  (∀ a ∉ s, f a = x) → (Filter.Tendsto f (l ⊓ Filter.principal s) (nhds x) ↔ Filter.Tendsto f l (nhds x))
-- Batteries.Data.AssocList
Batteries.AssocList.find?.eq_2 : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a a_1 : α) (b : β) (es : Batteries.AssocList α β),
  Batteries.AssocList.find? a (Batteries.AssocList.cons a_1 b es) =
    match a_1 == a with
    | true => some b
    | false => Batteries.AssocList.find? a es
-- Init.Data.List.Lemmas
List.mem_append_cons_self : ∀ {α : Type u_1} {xs : List α} {a : α} {ys : List α}, a ∈ xs ++ a :: ys
-- Lean.Util.Diff
/-- An action in an edit script to transform one source sequence into a target sequence.
 -/
Lean.Diff.Action : Type
-- Lean.Meta.PProdN
/-- Unpacks up to `n` elements from `PProd` tuple `e`.  Returns fewer if `e` has < `n` elements or
isn't a `PProd`. Returns `#[]` for `True`/`PUnit` or when `n = 0`.
 -/
Lean.Meta.PProdN.unpack : Lean.Expr → ℕ → Lean.MetaM (Array Lean.Expr)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.instCategory : {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} →
              {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)} →
                {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} →
                  CategoryTheory.Category.{max t v', max (max u' v') t} (F.DescentData' sq sq₃)
-- Init.Data.SInt.Bitwise
ISize.ofBitVec_not : ∀ (a : BitVec System.Platform.numBits), ISize.ofBitVec (~~~a) = ~~~ISize.ofBitVec a
-- Mathlib.Algebra.Algebra.Operations
Submodule.comap_op_pow : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (n : ℕ)
  (M : Submodule R Aᵐᵒᵖ),
  Submodule.comap (↑(MulOpposite.opLinearEquiv R)) (M ^ n) = Submodule.comap (↑(MulOpposite.opLinearEquiv R)) M ^ n
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.mk.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Monoid.Coprod.mk = (Monoid.coprodCon M N).mk'
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.equivI_apply_coe : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (a : h.ι), ↑(h.equivI a) = h.type₁ a
-- Mathlib.Algebra.Group.TransferInstance
Equiv.addSemigroup.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : AddSemigroup β],
  e.addSemigroup = Function.Injective.addSemigroup ⇑e ⋯ ⋯
-- Init.Data.Fin.Lemmas
/-- Proves a statement by reverse induction on the underlying `Nat` value in a `Fin (n + 1)`.

For the induction:
* `last` is the base case, demonstrating `motive (Fin.last n)`.
* `cast` is the inductive step, assuming the motive for `(j : Fin n).succ` and demonstrating it for
   the predecessor `j.castSucc`.

`Fin.induction` is the non-reverse induction principle.
 -/
Fin.reverseInduction : {n : ℕ} →
  {motive : Fin (n + 1) → Sort u_1} →
    motive (Fin.last n) → ((i : Fin n) → motive i.succ → motive i.castSucc) → (i : Fin (n + 1)) → motive i
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.Precoverage.IsStableUnderSup.of_preZeroHypercoverFamily : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.PreZeroHypercoverFamily C},
  (∀ ⦃X : C⦄ ⦃E F : CategoryTheory.PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)) →
    P.precoverage.IsStableUnderSup
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.continuous_union : ∀ {α : Type u_1} [inst : TopologicalSpace α], Continuous fun x => x.1 ∪ x.2
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.piecewise.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α}
  [inst : DecidablePred fun x => x ∈ s] (hs : MeasurableSet s) (κ η : ProbabilityTheory.Kernel α β),
  ProbabilityTheory.Kernel.piecewise hs κ η = { toFun := fun a => if a ∈ s then κ a else η a, measurable' := ⋯ }
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.hom.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b),
  Algebra.Generators.PresentationOfFreeCotangent.Aux.hom✝ D =
    Ideal.Quotient.liftₐ
      (Ideal.span (Set.range (Subtype.val ∘ Algebra.Generators.PresentationOfFreeCotangent.Aux.f✝ D ∘ ⇑b)))
      (MvPolynomial.aeval P.val) ⋯