mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.zero_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Zero Y] (x : X), 0 x = 0
-- Init.System.IO
/-- Returns the thread ID of the calling thread.  -/
IO.getTID : BaseIO UInt64
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The generic case of the first simplicial identity  -/
CategoryTheory.SimplicialObject.δ_comp_δ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i j : Fin (n + 2)},
  i ≤ j →
    ∀ {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.δ j.succ) (CategoryTheory.CategoryStruct.comp (X.δ i) h) =
        CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (CategoryTheory.CategoryStruct.comp (X.δ j) h)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.euclidean.integerLattice.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.euclidean.integerLattice K =
    ZLattice.comap ℝ (NumberField.mixedEmbedding.integerLattice K) ↑↑(NumberField.mixedEmbedding.euclidean.toMixed K)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instPreorder : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Preorder β] → Preorder (MeasureTheory.SimpleFunc α β)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- This is a technical result to ensure that the image of the `ℂ`-basis of `ℂ^n` defined in
`canonicalEmbedding.latticeBasis` is a `ℝ`-basis of the mixed space `ℝ^r₁ × ℂ^r₂`,
see `mixedEmbedding.latticeBasis`.  -/
NumberField.mixedEmbedding.disjoint_span_commMap_ker : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Disjoint (Submodule.span ℝ (Set.range ⇑(NumberField.canonicalEmbedding.latticeBasis K)))
    (NumberField.mixedEmbedding.commMap K).ker
-- Mathlib.Data.Set.Semiring
/-- The identity function `SetSemiring α → Set α`.  -/
SetSemiring.down : {α : Type u_1} → SetSemiring α ≃ Set α
-- Mathlib.Order.Monotone.Defs
Function.Injective.of_eq_imp_le : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] {f : α → β}, (∀ {x y : α}, f x = f y → x ≤ y) → Function.Injective f
-- Mathlib.Topology.NhdsWithin
nhdsWithin_inter' : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) (s t : Set α),
  nhdsWithin a (s ∩ t) = nhdsWithin a s ⊓ Filter.principal t
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.smulFDeriv_J_mul : ∀ (g : GL (Fin 2) ℝ) (z : ℂ),
  UpperHalfPlane.smulFDeriv (UpperHalfPlane.J * g) z = -↑Complex.conjCLE ∘SL UpperHalfPlane.smulFDeriv g z
-- Std.Internal.UV.TCP
/-- Receives data from a TCP socket with a maximum size of size bytes. The promise resolves when data is
available or an error occurs. If data is received, it’s wrapped in .some. If EOF is reached, the
result is .none, indicating no more data is available. Receiving data in parallel on the same
socket is not supported. Instead, we recommend binding multiple sockets to the same address.
Furthermore calling this function in parallel with `waitReadable` is not supported.
 -/
Std.Internal.UV.TCP.Socket.recv? : Std.Internal.UV.TCP.Socket → UInt64 → IO (IO.Promise (Except IO.Error (Option ByteArray)))
-- Lean.Server.CodeActions.Provider
Lean.CodeAction.FindTacticResult.tactic.sizeOf_spec : ∀ (a : Lean.Syntax.Stack), sizeOf (Lean.CodeAction.FindTacticResult.tactic a) = 1 + sizeOf a
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The defining property of the weak operator topology: a function `f` tends to
`A : E →WOT[𝕜] F` along filter `l` iff `y (f a x)` tends to `y (A x)` along the same filter.  -/
ContinuousLinearMapWOT.tendsto_iff_forall_dual_apply_tendsto : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] {α : Type u_5} {l : Filter α} {f : α → E →SWOT[σ] F} {A : E →SWOT[σ] F},
  Filter.Tendsto f l (nhds A) ↔
    ∀ (x : E) (y : StrongDual 𝕜₂ F), Filter.Tendsto (fun a => y ((f a) x)) l (nhds (y (A x)))
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.instFunLike : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} → FunLike (ContIntertwiningMap π₁ π₂) V W
-- Mathlib.Data.Fin.VecNotation
/-- Use `![...]` notation for displaying a vector `Fin n → α`, for example:

```
#eval ![1, 2] + ![3, 4] -- ![4, 6]
```
 -/
PiFin.hasRepr : {α : Type u} → {n : ℕ} → [Repr α] → Repr (Fin n → α)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Assumes right strict covariance.  -/
Right.mul_lt_mul_of_nonneg : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b c d : α} [inst_1 : Preorder α] [PosMulMono α] [MulPosStrictMono α],
  a < b → c < d → 0 ≤ a → 0 ≤ c → a * c < b * d
-- Mathlib.Topology.Algebra.Algebra
instContinuousMulElemIcoOfNat : ∀ (A : Type u) [inst : Semiring A] [inst_1 : TopologicalSpace A] [inst_2 : PartialOrder A] [inst_3 : IsOrderedRing A]
  [ContinuousMul A], ContinuousMul ↑(Set.Ico 0 1)
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.mk : {α : Type u_5} →
  (toField : Field α) →
    (toConditionallyCompleteLinearOrder : ConditionallyCompleteLinearOrder α) →
      [toIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid α] →
        [toZeroLEOneClass : ZeroLEOneClass α] →
          [toPosMulStrictMono : PosMulStrictMono α] →
            [toMulPosStrictMono : MulPosStrictMono α] → ConditionallyCompleteLinearOrderedField α
-- Mathlib.Tactic.GRewrite.Core
/-- When `useRewrite = true`, switch to using the default `rewrite` tactic when the goal is
and equality or iff.  -/
Mathlib.Tactic.GRewrite.Config.useRewrite : Mathlib.Tactic.GRewrite.Config → Bool
-- Mathlib.LinearAlgebra.Dimension.Free
Module.basisUnique_repr_eq_zero_iff : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : StrongRankCondition R] {ι : Type u_2} [inst_5 : Unique ι]
  {h : Module.finrank R M = 1} {v : M} {i : ι}, ((Module.basisUnique ι h).repr v) i = 0 ↔ v = 0
-- Mathlib.Probability.Moments.MGFAnalytic
/-- The moment-generating function is analytic at every `t ∈ interior (integrableExpSet X μ)`.  -/
ProbabilityTheory.analyticAt_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ∈ interior (ProbabilityTheory.integrableExpSet X μ) → AnalyticAt ℝ (ProbabilityTheory.mgf X μ) t
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.isNilpotent_trace_of_isNilpotent : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {M : Matrix n n R},
  IsNilpotent M → IsNilpotent M.trace
-- Init.PropLemmas
/-- If two if-then-else statements only differ by the `Decidable` instances, they are equal.  -/
ite_eq_ite : ∀ {α : Sort u_1} (p : Prop) {h h' : Decidable p} (x y : α), ((if p then x else y) = if p then x else y) ↔ True
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_mk : ∀ {α : Type u_1} [inst : LE α] (s : Set α) (hs : IsUpperSet s), ↑{ carrier := s, upper' := hs } = s
-- Mathlib.NumberTheory.Padics.PadicNumbers
Int.padicValuation_eq_zero_iff : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {x : ℤ}, (Int.padicValuation p) x = 0 ↔ x = 0
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.isUnit_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {a : M}, IsUnit (Associates.mk a) ↔ IsUnit a
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orInR.sizeOf_spec : ∀ (p : Mathlib.Tactic.ITauto.Proof), sizeOf p.orInR = 1 + sizeOf p
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.map_fst_toList_eq_keys : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → List.map Prod.fst m.toList = m.keys
-- Mathlib.Tactic.Simproc.Divisors
_private.Mathlib.Tactic.Simproc.Divisors.0.Nat.properDivisors_ofNat.unsafe_1 : ℕ → List ℕ
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp_cons : ∀ (f fs : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.codeSupp (f.cons fs) k =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal (f.cons fs) k) ∪
      Turing.PartrecToTM2.codeSupp f (Turing.PartrecToTM2.Cont'.cons₁ fs k)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a fallback : α}, m.contains a = false → m.getKeyD a fallback = fallback
-- Mathlib.CategoryTheory.Limits.Sifted
/-- A functor admitting a final functor from a sifted category is sifted.  -/
CategoryTheory.IsSifted.of_final_functor_from_sifted : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  [h₁ : CategoryTheory.IsSifted C] (F : CategoryTheory.Functor C D) [F.Final], CategoryTheory.IsSifted D
-- Mathlib.Algebra.Homology.DerivedCategory.Fractions
/-- Any morphism `f : Q.obj X ⟶ Q.obj Y` in the derived category can be written
as `f = Q.map g ≫ inv (Q.map s)` with `g : X ⟶ Y'` and `s : Y ⟶ Y'` a quasi-isomorphism.  -/
DerivedCategory.left_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {X Y : CochainComplex C ℤ} (f : DerivedCategory.Q.obj X ⟶ DerivedCategory.Q.obj Y),
  ∃ Y' g s,
    ∃ (x : CategoryTheory.IsIso (DerivedCategory.Q.map s)),
      f = CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map g) (CategoryTheory.inv (DerivedCategory.Q.map s))
-- Mathlib.Data.Finset.Insert
Finset.mk_cons : ∀ {α : Type u_1} {a : α} {s : Multiset α} (h : (a ::ₘ s).Nodup),
  { val := a ::ₘ s, nodup := h } = Finset.cons a { val := s, nodup := ⋯ } ⋯
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfLEArgs.max_eq : ∀ {α : Type u} (self : Std.Packages.LinearOrderOfLEArgs α),
  let this := self.le;
  let this_1 := self.decidableLE;
  let this_2 := self.max;
  ∀ (a b : α), a ⊔ b = if b ≤ a then a else b
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.generate_of_singleton_isSplitEpi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.IsSplitEpi f],
  CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton f) = ⊤
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instT0Space : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] [T0Space R], T0Space (ContinuousMapZero X R)
-- Mathlib.LinearAlgebra.Ray
/-- An induction principle for `Module.Ray`, used as `induction x using Module.Ray.ind`.  -/
Module.Ray.ind : ∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {C : Module.Ray R M → Prop},
  (∀ (v : M) (hv : v ≠ 0), C (rayOfNeZero R v hv)) → ∀ (x : Module.Ray R M), C x
-- Batteries.Lean.EStateM
EStateM.run'_get : ∀ {σ ε : Type u_1} (s : σ), get.run' s = some s
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.contractLeft_one : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (d : Module.Dual R M), (CliffordAlgebra.contractLeft d) 1 = 0
-- Mathlib.Order.SuccPred.Basic
/-- See also `Order.pred_eq_of_covBy`.  -/
Order.pred_le_of_wcovBy : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, b ⩿ a → Order.pred a ≤ b
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.le_boundedBy' : ∀ {α : Type u_1} {m : Set α → ENNReal} {μ : MeasureTheory.OuterMeasure α},
  μ ≤ MeasureTheory.OuterMeasure.boundedBy m ↔ ∀ (s : Set α), s.Nonempty → μ s ≤ m s
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.distribMulActionHom_ext'_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] {N : Type u_7} [inst_1 : Monoid R]
  [inst_2 : AddMonoid N] [inst_3 : DistribMulAction R N] [inst_4 : DistribMulAction R S]
  {f g : MonoidAlgebra S M →+[R] N},
  f = g ↔
    ∀ (a : M), f.comp (MonoidAlgebra.singleDistribMulActionHom a) = g.comp (MonoidAlgebra.singleDistribMulActionHom a)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instInhabited : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → [Inhabited A] → Inhabited (CStarMatrix m n A)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_iff_isSome_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {a : α},
  a ∈ t ↔ (t.get? a).isSome = true
-- Mathlib.Algebra.Algebra.Defs
algebraMap.smul' : ∀ {A : Type u_1} {B : Type u_2} (a : A) (b : B) (C : Type u_3) [inst : SMul A B] [inst_1 : CommSemiring B]
  [inst_2 : Semiring C] [inst_3 : Algebra B C] [inst_4 : Monoid A] [inst_5 : MulDistribMulAction A C]
  [SMulDistribClass A B C], (algebraMap B C) (a • b) = a • (algebraMap B C) b
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
/-- The `S`-linear map on the span of roots given by evaluating at a coroot.  -/
RootPairing.coroot'In : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (P : RootPairing ι R M N) →
                    (S : Type u_6) →
                      [inst_5 : CommRing S] →
                        [inst_6 : Algebra S R] →
                          [inst_7 : Module S M] →
                            [IsScalarTower S R M] →
                              [FaithfulSMul S R] → [P.IsValuedIn S] → ι → Module.Dual S ↥(P.rootSpan S)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.succMany?_eq : ∀ {n : ℕ} {α : Type u} [Std.PRange.UpwardEnumerable α] [inst : LE α] [inst_1 : LT α] [m : HasModel✝ α (BitVec n)]
  {x : α} {k : ℕ},
  Std.PRange.succMany? k x =
    if (HasModel.encode✝ x).toInt + ↑k ≤ (BitVec.Signed.intMaxSealed✝ n).toInt then
      some (HasModel.decode✝ (BitVec.ofInt n ((HasModel.encode✝ x).toInt + ↑k)))
    else none
-- Mathlib.Algebra.Tropical.Basic
Tropical.add_eq_right : ∀ {R : Type u} [inst : LinearOrder R] ⦃x y : Tropical R⦄, y ≤ x → x + y = y
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- A single function is uniformly integrable in the probability sense.  -/
MeasureTheory.uniformIntegrable_subsingleton : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β} [Subsingleton ι],
  1 ≤ p → p ≠ ⊤ → (∀ (i : ι), MeasureTheory.MemLp (f i) p μ) → MeasureTheory.UniformIntegrable f p μ
-- Mathlib.Order.UpperLower.Closure
upperClosure_union : ∀ {α : Type u_1} [inst : Preorder α] (s t : Set α), upperClosure (s ∪ t) = upperClosure s ⊓ upperClosure t
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.expand.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α] (data_2 : Array (Std.DHashMap.Internal.AssocList α β))
  (hd : 0 < data_2.size),
  Std.DHashMap.Internal.Raw₀.expand ⟨data_2, hd⟩ =
    Std.DHashMap.Internal.Raw₀.expand.go✝ 0 data_2
      ⟨Array.replicate (data_2.size * 2) Std.DHashMap.Internal.AssocList.nil, ⋯⟩
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with
at least as many pigeons as the ceiling of the average number of pigeons across all pigeonholes.  -/
Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {b : M}
  [inst_1 : CommSemiring M] [inst_2 : LinearOrder M] [IsStrictOrderedRing M],
  (∀ a ∈ s, f a ∈ t) → t.card • b < ↑s.card → ∃ y ∈ t, b < ↑{x ∈ s | f x = y}.card
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.instInhabitedValueGroup : (A : Type u) →
  [inst : CommRing A] →
    (K : Type v) → [inst_1 : Field K] → [inst_2 : Algebra A K] → Inhabited (ValuationRing.ValueGroup A K)
-- Lean.Meta.Tactic.NormCast
/-- Counts how many coercions are inside the expression, including the head ones.  -/
Lean.Meta.NormCast.countCoes : Lean.Expr → Lean.MetaM ℕ
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections.congr_simp : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f f_1 : A →+* ↑(X.presheaf.obj (Opposite.op ⊤)))
  (e_f : f = f_1) {x : ↑(X.presheaf.obj (Opposite.op ⊤))} {t : A} {d d_1 : ℕ} (e_d : d = d_1) (H : f t = x)
  (h0d : 0 < d) (hd : t ∈ 𝒜 d),
  AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections 𝒜 f H h0d hd =
    AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections 𝒜 f_1 ⋯ ⋯ ⋯
-- Mathlib.Order.Heyting.Basic
ofDual_hnot : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : αᵒᵈ), OrderDual.ofDual (￢a) = (OrderDual.ofDual a)ᶜ
-- Mathlib.CategoryTheory.UnivLE
instIsEquivalenceUliftFunctorOfUnivLE : ∀ [UnivLE.{max u v, v}], CategoryTheory.uliftFunctor.{u, v}.IsEquivalence
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderBaseChange], P.op.IsStableUnderCobaseChange
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The machine states for a TM1 emulating a TM0 machine. States of the TM0 machine are embedded
as `normal q` states, but the actual operation is split into two parts, a jump to `act s q`
followed by the action and a jump to the next `normal` state.  -/
Turing.TM0to1.Λ' : Type u_1 → Type u_2 → Type (max u_1 u_2)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.core.injEq : ∀ (a b : Lean.Expr) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) (a_1 b_1 : Lean.Expr)
  (lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr),
  (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.core a b lhs rhs =
      Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.core a_1 b_1 lhs_1 rhs_1) =
    (a = a_1 ∧ b = b_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor for additive groups is full.  -/
AddGrpCat.instFullUliftFunctor : AddGrpCat.uliftFunctor.Full
-- Mathlib.Logic.Relation
Relation.comp_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → β → Prop} {p : β → γ → Prop} {q : γ → δ → Prop},
  Relation.Comp (Relation.Comp r p) q = Relation.Comp r (Relation.Comp p q)
-- Mathlib.Order.Restriction
/-- Restrict domain of a function `f` indexed by `α` to elements `≤ a`.  -/
Preorder.restrictLe : {α : Type u_1} → [inst : Preorder α] → {π : α → Type u_2} → (a : α) → ((a : α) → π a) → (a_1 : ↑(Set.Iic a)) → π ↑a_1
-- Mathlib.Analysis.Analytic.Order
/-- The derivative of an analytic function `f` has infinite analytic order at a zero `z₀` if and
only if `f` has infinite analytic order at `z₀`.  -/
analyticOrderAt_deriv_eq_top_iff_of_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CharZero 𝕜] [CompleteSpace E] {z₀ : 𝕜} {f : 𝕜 → E},
  AnalyticAt 𝕜 f z₀ → f z₀ = 0 → (analyticOrderAt (deriv f) z₀ = ⊤ ↔ analyticOrderAt f z₀ = ⊤)
-- Mathlib.Logic.Equiv.Fin.Rotate
finRotate_succ_apply : ∀ {n : ℕ} (i : Fin (n + 1)), (finRotate (n + 1)) i = i + 1
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A}
  (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) (X : Aᵒᵖ),
  (CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom α).app X =
    CategoryTheory.Functor.IsCoverDense.Types.presheafHom
      (CategoryTheory.Functor.IsCoverDense.homOver α (Opposite.unop X))
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.KerLift.map_smul : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Semiring B] [inst_4 : Algebra R₁ B] (f : A →ₐ[R₁] B) (r : R₁) (x : A ⧸ RingHom.ker f),
  f.kerLift (r • x) = r • f.kerLift x
-- Mathlib.Data.Finset.NAry
Finset.image₂_subset_iff_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  {u : Finset γ}, Finset.image₂ f s t ⊆ u ↔ ∀ a ∈ s, Finset.image (fun b => f a b) t ⊆ u
-- Mathlib.LinearAlgebra.RootSystem.OfBilinear
LinearMap.IsReflective.isOrthogonal_reflection : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (B : M →ₗ[R] M →ₗ[R] R) {x : M} (hx : B.IsReflective x), B.IsSymm → B.IsOrthogonal ⇑(Module.reflection ⋯)
-- Mathlib.NumberTheory.Modular
/-- If `z ∈ 𝒟` and `z ≠ I, ρ, 1 + ρ`, then the stabilizer of `z` in `SL(2, ℤ)` is `± 1`.  -/
ModularGroup.stabilizer_of_ne : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane},
  z ∈ ModularGroup.fd →
    g • z = z → z ≠ UpperHalfPlane.I → z ≠ UpperHalfPlane.ρ → z ≠ 1 +ᵥ UpperHalfPlane.ρ → g = 1 ∨ g = -1
-- Mathlib.Order.SymmDiff
bihimp_le_iff_left : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), bihimp a b ≤ a ↔ Codisjoint a b
-- Mathlib.Logic.ExistsUnique
/-- `∃! x : α, p x` means that there exists a unique `x` in `α` such that `p x`.
This is notation for `ExistsUnique (fun (x : α) ↦ p x)`.

This notation does not allow multiple binders like `∃! (x : α) (y : β), p x y`
as a shorthand for `∃! (x : α), ∃! (y : β), p x y` since it is liable to be misunderstood.
Often, the intended meaning is instead `∃! q : α × β, p q.1 q.2`.
 -/
Mathlib.Notation.«term∃!_,_» : Lean.ParserDescr
-- Lean.Data.KVMap
Lean.instCoeNatDataValue : Coe ℕ Lean.DataValue
-- Mathlib.Order.OmegaCompletePartialOrder
Prod.instOmegaCompletePartialOrder : {α : Type u_2} →
  {β : Type u_3} → [OmegaCompletePartialOrder α] → [OmegaCompletePartialOrder β] → OmegaCompletePartialOrder (α × β)
-- Mathlib.Order.SymmDiff
symmDiff_of_le : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ b → symmDiff a b = b \ a
-- Mathlib.Algebra.FiniteSupport.Defs
/-- The function `f` has finite multiplicative support.  -/
Function.HasFiniteMulSupport : {α : Type u_1} → {M : Type u_2} → [One M] → (α → M) → Prop
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.mk : {M : Type u_2} →
  {N : Type u_3} →
    {φ : M → N} →
      {X : Type u_5} →
        [inst : SMul M X] →
          {Y : Type u_6} →
            [inst_1 : SMul N Y] → (toFun : X → Y) → (∀ (m : M) (x : X), toFun (m • x) = φ m • toFun x) → X →ₑ[φ] Y
-- Mathlib.MeasureTheory.Measure.Support
/-- The support of the sum of two measures is the union of the supports.  -/
MeasureTheory.Measure.support_add : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] (μ ν : MeasureTheory.Measure X),
  (μ + ν).support = μ.support ∪ ν.support
-- Mathlib.Algebra.Ring.Defs
Ring.zsmul_succ' : ∀ {R : Type u} [self : Ring R] (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a