mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Adjunction
CategoryTheory.Sheaf.adjunction_counit_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [inst_3 : CategoryTheory.HasWeakSheafify J D]
  [inst_4 : J.HasSheafCompose F] (adj : G ⊣ F) (Y : CategoryTheory.Sheaf J D),
  ((CategoryTheory.Sheaf.adjunction J adj).counit.app Y).hom =
    CategoryTheory.sheafifyLift J ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).counit.app Y.obj) ⋯
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.zmultiples_isAddCommutative : ∀ {G : Type u_1} [inst : AddGroup G] (g : G), IsAddCommutative ↥(AddSubgroup.zmultiples g)
-- Init.Data.Float.Float32
/-- 32-bit floating-point numbers.

`Float32` corresponds to the IEEE 754 *binary32* format (`float` in C or `f32` in Rust).
Floating-point numbers are a finite representation of a subset of the real numbers, extended with
extra “sentinel” values that represent undefined and infinite results as well as separate positive
and negative zeroes. Arithmetic on floating-point numbers approximates the corresponding operations
on the real numbers by rounding the results to numbers that are representable, propagating error and
infinite values.

Floating-point numbers include [subnormal numbers](https://en.wikipedia.org/wiki/Subnormal_number).
Their special values are:
 * `NaN`, which denotes a class of “not a number” values that result from operations such as
   dividing zero by zero, and
 * `Inf` and `-Inf`, which represent positive and infinities that result from dividing non-zero
   values by zero.

Like other low-level types, `Float32` is special-cased by the Lean compiler to correspond to the C
`float` type. From the point of view of Lean's logic, `Float32` is equivalent to `Float32.Model`
(via the functions `Float32.toModel` and `Float32.ofModel`), which is itself a subtype of `UInt32`.
Some of the operations on `Float32` are defined in terms of their `Float32.Model` counterparts,
while others are opaque to Lean's kernel.
 -/
Float32 : Type
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.id.match_1.splitter : {C : Type u_1} →
  (motive : CategoryTheory.WithInitial C → Sort u_2) →
    (x : CategoryTheory.WithInitial C) →
      ((a : C) → motive (CategoryTheory.WithInitial.of a)) → (Unit → motive CategoryTheory.WithInitial.star) → motive x
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Param : Lean.Compiler.LCNF.Purity → Type
-- Mathlib.Data.Set.Lattice
Set.biUnion_of_singleton : ∀ {α : Type u_1} (s : Set α), ⋃ x ∈ s, {x} = s
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Given a function `f : ι → M` and a finite set `t ⊆ ι`, we can always find `i : ι`, belonging to `t`
if `t` is nonempty, such that `‖∏ j ∈ t, f j‖ ≤ ‖f i‖`.
 -/
IsUltrametricDist.exists_norm_finsetProd_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] (t : Finset ι) [Nonempty ι]
  (f : ι → M), ∃ i, (t.Nonempty → i ∈ t) ∧ ‖∏ j ∈ t, f j‖ ≤ ‖f i‖
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The right-hand side of the diagram commutes.  -/
AddGroupExtension.Equiv.rightHom_comm : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G}
  (self : S.Equiv S'), ⇑S'.rightHom ∘ ⇑self.toAddEquiv = ⇑S.rightHom
-- Mathlib.NumberTheory.Divisors
Int.divisorsAntidiag_neg_natCast : ∀ (n : ℕ),
  (-↑n).divisorsAntidiag =
    (Finset.map (Nat.castEmbedding.prodMap (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))))
          n.divisorsAntidiagonal).disjUnion
      (Finset.map ((Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))).prodMap Nat.castEmbedding)
        n.divisorsAntidiagonal)
      ⋯
-- Mathlib.RingTheory.MvPolynomial.Ideal
MvPolynomial.pow_idealOfVars : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (n : ℕ),
  MvPolynomial.idealOfVars σ R ^ n = MvPolynomial.restrictSupportIdeal R (⇑Finsupp.degree ⁻¹' Set.Ici n) ⋯
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.inv_left : ∀ {D : Type u_1} {Q : Type u_2} [inst : Group D] [inst_1 : Group Q] (a : D ≀ᵣ Q),
  a⁻¹.left = fun x => a.left⁻¹ (a.right * x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_le_size_insertManyIfNewUnit_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] (h : t.WF)
  {l : List α}, t.size ≤ (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).size
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption : Type
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.commRingEquiv.eq_1 : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N],
  MonoidAlgebra.commRingEquiv =
    MonoidAlgebra.curryRingEquiv.symm.trans
      ((MonoidAlgebra.mapDomainRingEquiv R MulEquiv.prodComm).trans MonoidAlgebra.curryRingEquiv)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- For any circle integrable function `f`, the power series `cauchyPowerSeries f c R`, `R > 0`,
converges to the Cauchy integral `(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z` on the open
disc `Metric.ball c R`.  -/
hasFPowerSeriesOn_cauchy_integral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : NNReal},
  CircleIntegrable f c ↑R →
    0 < R →
      HasFPowerSeriesOnBall (fun w => (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z)
        (cauchyPowerSeries f c ↑R) c ↑R
-- Mathlib.Order.ULift
ULift.down_lt : ∀ {α : Type u} [inst : LT α] {a b : ULift.{u_1, u} α}, a.down < b.down ↔ a < b
-- Mathlib.Algebra.Group.Center
Set.addCentralizer_union : ∀ {M : Type u_1} {S T : Set M} [inst : Add M], (S ∪ T).addCentralizer = S.addCentralizer ∩ T.addCentralizer
-- Mathlib.CategoryTheory.Sites.Spaces
Opens.coversTop_iff : ∀ (T : Type u) [inst : TopologicalSpace T] {ι : Type u_1} (U : ι → TopologicalSpace.Opens T),
  (Opens.grothendieckTopology T).CoversTop U ↔ TopologicalSpace.IsOpenCover U
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.ForgetEnrichment.equiv_inverse : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {D : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} D] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V D],
  (CategoryTheory.ForgetEnrichment.equiv V).inverse = CategoryTheory.ForgetEnrichment.equivInverse V D
-- Init.Data.List.Find
List.findIdx?_eq_none_iff : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, List.findIdx? p xs = none ↔ ∀ x ∈ xs, p x = false
-- Mathlib.RingTheory.Adjoin.Basic
Algebra.adjoin_adjoin_of_tower : ∀ (R : Type uR) {S : Type uS} {A : Type uA} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] (s : Set A),
  Algebra.adjoin S ↑(Algebra.adjoin R s) = Algebra.adjoin S s
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
/-- Left division by a nonzero element in a `CommGroupWithZero` is a permutation of the underlying
type.  -/
Equiv.divLeft₀ : {G₀ : Type u_1} → [inst : CommGroupWithZero G₀] → (a : G₀) → a ≠ 0 → Equiv.Perm G₀
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l → k ∈ List.map Sigma.fst l → (m.insertMany l).getKey! k' = k
-- Mathlib.Topology.Algebra.WithZeroTopology
WithZeroTopology.Iio_mem_nhds : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {γ₁ γ₂ : Γ₀}, γ₁ < γ₂ → Set.Iio γ₂ ∈ nhds γ₁
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.of'_divOf : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G] (a : G),
  (AddMonoidAlgebra.of' k G a).divOf a = 1
-- Mathlib.Analysis.Real.Pi.Bounds
Real.round_pi_eq_three : round Real.pi = 3
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.apply_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [inst_8 : ContinuousConstSMul 𝕜 F]
  [inst_9 : ContinuousSMul 𝕜 E] {m : ι → E} {c : E [⋀^ι]→L[𝕜] F}, (ContinuousAlternatingMap.apply 𝕜 E F m) c = c m
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.TM2.step.match_1.splitter : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        (motive : Turing.TM2.Cfg Γ Λ σ → Sort u_5) →
          (x : Turing.TM2.Cfg Γ Λ σ) →
            ((var : σ) → (stk : (k : K) → List (Γ k)) → motive { l := none, var := var, stk := stk }) →
              ((l : Λ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive { l := some l, var := v, stk := S }) → motive x
-- Mathlib.Algebra.Group.Int.Even
Int.even_sub : ∀ {m n : ℤ}, Even (m - n) ↔ (Even m ↔ Even n)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isoSpec_Spec : ∀ (R : CommRingCat),
  (AlgebraicGeometry.Spec R).isoSpec = AlgebraicGeometry.Scheme.Spec.mapIso (AlgebraicGeometry.Scheme.ΓSpecIso R).op
-- Init.MetaTypes
/-- When `true` (default : `true`), then `simp` will remove unused `let` and `have` expressions:
`let x := v; e` simplifies to `e` when `x` does not occur in `e`.
 -/
Lean.Meta.DSimp.Config.zetaUnused : Lean.Meta.DSimp.Config → Bool
-- Mathlib.Analysis.Seminorm
Seminorm.instInhabited : {𝕜 : Type u_3} →
  {E : Type u_7} → [inst : SeminormedRing 𝕜] → [inst_1 : AddGroup E] → [inst_2 : SMul 𝕜 E] → Inhabited (Seminorm 𝕜 E)
-- Mathlib.Data.UInt
UInt64.toBitVec_nsmul : ∀ (n : ℕ) (a : UInt64), (n • a).toBitVec = n • a.toBitVec
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `self_subset_setOfPred_gauge_le_one`. -/
self_subset_setOf_gauge_le_one : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E}, s ⊆ {x | gauge s x ≤ 1}
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- the adjunction  -/
CategoryTheory.Bicategory.Adj.Hom.adj : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} → (self : CategoryTheory.Bicategory.Adj.Hom a b) → CategoryTheory.Bicategory.Adjunction self.l self.r
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.LiftRelAux.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ Computation α → β ⊕ Computation β → Sort u_3) (a : α) (b : β)
  (h_1 : (a : α) → (b : β) → motive (Sum.inl a) (Sum.inl b))
  (h_2 : (a : α) → (cb : Computation β) → motive (Sum.inl a) (Sum.inr cb))
  (h_3 : (ca : Computation α) → (b : β) → motive (Sum.inr ca) (Sum.inl b))
  (h_4 : (ca : Computation α) → (cb : Computation β) → motive (Sum.inr ca) (Sum.inr cb)),
  (match Sum.inl a, Sum.inl b with
    | Sum.inl a, Sum.inl b => h_1 a b
    | Sum.inl a, Sum.inr cb => h_2 a cb
    | Sum.inr ca, Sum.inl b => h_3 ca b
    | Sum.inr ca, Sum.inr cb => h_4 ca cb) =
    h_1 a b
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_eq_zero_iff : ∀ (x y : ℂ), x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
-- Mathlib.Data.Set.Basic
SetCoe.ext_iff : ∀ {α : Type u} {s : Set α} {a b : ↑s}, ↑a = ↑b ↔ a = b
-- Mathlib.Algebra.Order.ToIntervalMod
QuotientAddGroup.circularPreorder : {α : Type u_1} →
  [inst : AddCommGroup α] →
    [inst_1 : LinearOrder α] →
      [IsOrderedAddMonoid α] →
        [hα : Archimedean α] → {p : α} → [hp' : Fact (0 < p)] → CircularPreorder (α ⧸ AddSubgroup.zmultiples p)
-- Mathlib.Topology.Order.OrderClosed
/-- The set of monotone functions on a set is closed.  -/
isClosed_monotoneOn : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
  [inst_2 : Preorder β] {s : Set β}, IsClosed {f | MonotoneOn f s}
-- Init.Data.Int.Gcd
Int.gcd_le_right : ∀ {b : ℤ} (a : ℤ), 0 < b → ↑(a.gcd b) ≤ b
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_bot : ∀ {M : Type u_2} [inst : Mul M], ⊥.op = ⊥
-- Mathlib.Topology.Compactness.Lindelof
IsLindeof.compl_mem_coclosedLindelof_of_isClosed : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsLindelof s → IsClosed s → sᶜ ∈ Filter.coclosedLindelof X
-- Mathlib.Algebra.Homology.Localization
/-- The functor `F.mapHomologicalComplexUpToQuasiIso c` is induced by
`F.mapHomologicalComplex c`.  -/
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactors : {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) →
          {ι : Type u_3} →
            (c : ComplexShape ι) →
              [inst_2 : CategoryTheory.Preadditive C] →
                [inst_3 : CategoryTheory.Preadditive D] →
                  [inst_4 : CategoryTheory.CategoryWithHomology C] →
                    [inst_5 : CategoryTheory.CategoryWithHomology D] →
                      [inst_6 : (HomologicalComplex.quasiIso D c).HasLocalization] →
                        [inst_7 : F.Additive] →
                          [inst_8 : F.PreservesHomology] →
                            [inst_9 : (HomologicalComplex.quasiIso C c).HasLocalization] →
                              HomologicalComplexUpToQuasiIso.Q.comp (F.mapHomologicalComplexUpToQuasiIso c) ≅
                                (F.mapHomologicalComplex c).comp HomologicalComplexUpToQuasiIso.Q
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_equiv_eq_comap_symm : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (f : M ≃* N) (K : Submonoid M),
  Submonoid.map f K = Submonoid.comap f.symm K
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Reindexing by `Equiv.refl` yields the original simplex.  -/
Affine.Simplex.reindex_refl : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n), s.reindex (Equiv.refl (Fin (n + 1))) = s
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.function : Lean.Lsp.SymbolKind
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_empty : ∀ (F : Type u_3) (E : Type u_4) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E], F⟮⟯ = ⊥
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.append.eq_2 : ∀ (p₂ : Int.Internal.Linear.Poly) (k : ℤ) (v : Int.Internal.Linear.Var) (p_1 : Int.Internal.Linear.Poly),
  (Int.Internal.Linear.Poly.add k v p_1).append p₂ = Int.Internal.Linear.Poly.add k v (p_1.append p₂)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The currying operation `Function.curry` as a measurable equivalence.
See `MeasurableEquiv.curry` for the non-dependent version.  -/
MeasurableEquiv.piCurry : {ι : Type u_6} →
  {κ : ι → Type u_7} →
    (X : (i : ι) → κ i → Type u_8) →
      [inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)] →
        ((p : (i : ι) × κ i) → X p.fst p.snd) ≃ᵐ ((i : ι) → (j : κ i) → X i j)
-- Mathlib.CategoryTheory.Preadditive.FunctorCategory
CategoryTheory.functorCategoryPreadditive : {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.Preadditive D] → CategoryTheory.Preadditive (CategoryTheory.Functor C D)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.diam_image : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (s : Set P),
  Metric.diam (⇑f '' s) = Metric.diam s
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.swapCompInl_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C), (CategoryTheory.Sum.swapCompInl C D).hom.app X = CategoryTheory.CategoryStruct.id (Sum.inr X)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.contains_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  (Std.ExtDHashMap.Const.alter m k f).contains k = (f (Std.ExtDHashMap.Const.get? m k)).isSome
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.step.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Λ] [inst_1 : Inhabited Γ] (M : Turing.TM0.Machine Γ Λ) (q : Λ)
  (T : Turing.Tape Γ),
  Turing.TM0.step M { q := q, Tape := T } =
    Option.map
      (fun x =>
        match x with
        | (q', a) =>
          { q := q',
            Tape :=
              match a with
              | Turing.TM0.Stmt.move d => Turing.Tape.move d T
              | Turing.TM0.Stmt.write a => Turing.Tape.write a T })
      (M q T.head)
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.Entry.mk.inj : ∀ {fromDeclName toDeclName thmName fromDeclName_1 toDeclName_1 thmName_1 : Lean.Name},
  { fromDeclName := fromDeclName, toDeclName := toDeclName, thmName := thmName } =
      { fromDeclName := fromDeclName_1, toDeclName := toDeclName_1, thmName := thmName_1 } →
    fromDeclName = fromDeclName_1 ∧ toDeclName = toDeclName_1 ∧ thmName = thmName_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.coe_inv_variableChange_Δ' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R)
  [inst_1 : W.IsElliptic], ↑(C • W).Δ'⁻¹ = ↑C.u ^ 12 * ↑W.Δ'⁻¹
-- Init.Data.Order.PackageFactories
/-- This structure contains all the data needed to create a `LinearPreorderPackage α` instance.
Its fields are automatically provided if possible. For the detailed rules how the fields are
inferred, see `LinearPreorderPackage.ofOrd`.
 -/
Std.Packages.LinearPreorderOfOrdArgs : Type u → Type u
-- Mathlib.Analysis.Calculus.Deriv.Inv
DifferentiableOn.div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'},
  DifferentiableOn 𝕜 c s → DifferentiableOn 𝕜 d s → (∀ x ∈ s, d x ≠ 0) → DifferentiableOn 𝕜 (c / d) s
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.isDiscrete_comap_preimage : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.QuasiFinite R S] {s : Set (PrimeSpectrum R)},
  IsDiscrete s → IsDiscrete (PrimeSpectrum.comap (algebraMap R S) ⁻¹' s)
-- Mathlib.Analysis.Convex.Hull
convexHull_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E], (convexHull 𝕜) ∅ = ∅
-- Mathlib.Analysis.Analytic.IteratedFDeriv
_private.Mathlib.Analysis.Analytic.IteratedFDeriv.0.FormalMultilinearSeries.iteratedFDerivSeries.match_1.splitter : (motive : ℕ → Sort u_1) → (k : ℕ) → (Unit → motive 0) → ((k : ℕ) → motive k.succ) → motive k
-- Mathlib.Order.Hom.Set
Set.InjOn.sumElim : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} {s : Set α × Set β},
  Set.InjOn f s.1 → Set.InjOn g s.2 → (∀ a ∈ s.1, ∀ b ∈ s.2, f a ≠ g b) → Set.InjOn (Sum.elim f g) (Set.sumEquiv.symm s)
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_le_iff : ∀ {X : AlgebraicGeometry.Scheme} {𝒰 : X.OpenCover} [inst : Preorder 𝒰.I₀],
  (∀ {i j : 𝒰.I₀},
      i ≤ j ↔ AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f i) ≤ AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f j)) →
    ∀ (i j : 𝒰.I₀),
      i ≤ j ↔ AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f i) ≤ AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f j)
-- Init.Data.Int.ToString
_private.Init.Data.Int.ToString.0.Int.repr.eq_2 : ∀ (m : ℕ), (Int.negSucc m).repr = "-" ++ m.succ.repr
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.map_nonZeroDivisors_le : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S], Submonoid.map (algebraMap R S) (nonZeroDivisors R) ≤ nonZeroDivisors S
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- As well as being linear, `ι Q` squares to the quadratic form  -/
CliffordAlgebra.ι_sq_scalar : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M),
  (CliffordAlgebra.ι Q) m * (CliffordAlgebra.ι Q) m = (algebraMap R (CliffordAlgebra Q)) (Q m)
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- A map `f` between modules over a semiring is linear if it satisfies the two properties
`f (x + y) = f x + f y` and `f (c • x) = c • f x`. The predicate `IsLinearMap R f` asserts this
property. A bundled version is available with `LinearMap`, and should be favored over
`IsLinearMap` most of the time.  -/
IsLinearMap : (R : Type u) →
  {M : Type v} →
    {M₂ : Type w} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : AddCommMonoid M₂] → [Module R M] → [Module R M₂] → (M → M₂) → Prop
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.mk.sizeOf_spec : ∀ {α : Type u_4} [inst : TopologicalSpace α] [inst_1 : SizeOf α] (carrier : Set α) (isCompact' : IsCompact carrier),
  sizeOf { carrier := carrier, isCompact' := isCompact' } = 1
-- Lean.Parser
Lean.PrettyPrinter.Formatter.scientificLit.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Expr
/-- Return the approximated depth of an expression. This information is used to compute
the expression hash code, and speedup comparisons.
This is a constant time operation. We say it is approximate because it maxes out at `255`.
 -/
Lean.Expr.approxDepth : Lean.Expr → UInt32
-- Init.Notation
/-- Configuration for the `#reduce` command.  -/
Lean.reduceConfig : Lean.ParserDescr
-- Batteries.Data.MLList.Basic
/-- Join a monadic lazy list of monadic lazy lists into a single monadic lazy list.  -/
MLList.join : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m (MLList m α) → MLList m α
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiff_of_discreteTopology : ∀ {𝕜 : 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'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {n : WithTop ℕ∞} [DiscreteTopology M], ContMDiff I I' n f
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_right_split_dvd_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℤ → Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.equiv_some_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {P : Fin 3 → F}, P 2 ≠ 0 → P ≈ ![P 0 / P 2 ^ 2, P 1 / P 2 ^ 3, 1]
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.colLen_transpose : ∀ (μ : YoungDiagram) (j : ℕ), μ.transpose.colLen j = μ.rowLen j
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
measurable_nnnorm : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup α] [OpensMeasurableSpace α], Measurable nnnorm
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_smul_of_not_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P Q : Fin 3 → R},
  ¬P ≈ Q → ∀ {u v : R}, IsUnit u → IsUnit v → W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q