mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkInductiveAux₂.eq_2 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1)
  (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 ⟶ Q.X 2)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1))
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X (n + 1)) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                  CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
              CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2)))
  (n : ℕ),
  Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ n.succ =
    ⟨CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P ⋯).hom
        (Homotopy.mkInductiveAux₁ e zero one comm_one succ n).fst,
      ⟨CategoryTheory.CategoryStruct.comp (Homotopy.mkInductiveAux₁ e zero one comm_one succ n).snd.fst
          (HomologicalComplex.xPrevIso Q ⋯).inv,
        ⋯⟩⟩
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinAt.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E},
  HasFPowerSeriesWithinAt f p s x → g =ᶠ[nhdsWithin x s] f → g x = f x → HasFPowerSeriesWithinAt g p s x
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.map_inv : ∀ {α β : Type u} (f : α → β) (x : FreeGroup α), f <$> x⁻¹ = (f <$> x)⁻¹
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If we have particular limit cones available for `E ⋙ F` and for `F`,
we obtain a formula for `limit.pre F E`.
 -/
CategoryTheory.Limits.limit.pre_eq : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasLimit F] {E : CategoryTheory.Functor K J}
  [inst_4 : CategoryTheory.Limits.HasLimit (E.comp F)] (s : CategoryTheory.Limits.LimitCone (E.comp F))
  (t : CategoryTheory.Limits.LimitCone F),
  CategoryTheory.Limits.limit.pre F E =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone t).hom
      (CategoryTheory.CategoryStruct.comp (s.isLimit.lift (CategoryTheory.Limits.Cone.whisker E t.cone))
        (CategoryTheory.Limits.limit.isoLimitCone s).inv)
-- Mathlib.ModelTheory.Complexity
_private.Mathlib.ModelTheory.Complexity.0.FirstOrder.Language.BoundedFormula.toPrenex.match_1.eq_4 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (x : ℕ)
  (f₁ f₂ : L.BoundedFormula α x) (h_1 : (x : ℕ) → motive x FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (x : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (x l : ℕ) →
      (R : L.Relations l) → (ts : Fin l → L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (x : ℕ) → (f₁ f₂ : L.BoundedFormula α x) → motive x (f₁.imp f₂))
  (h_5 : (x : ℕ) → (f : L.BoundedFormula α (x + 1)) → motive x f.all),
  (match x, f₁.imp f₂ with
    | x, FirstOrder.Language.BoundedFormula.falsum => h_1 x
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 x t₁ t₂
    | x, FirstOrder.Language.BoundedFormula.rel R ts => h_3 x l R ts
    | x, f₁.imp f₂ => h_4 x f₁ f₂
    | x, f.all => h_5 x f) =
    h_4 x f₁ f₂
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- `Complex.conj` is analogous to `CliffordAlgebra.involute`.  -/
CliffordAlgebraComplex.ofComplex_conj : ∀ (c : ℂ),
  CliffordAlgebraComplex.ofComplex ((starRingEnd ℂ) c) = CliffordAlgebra.involute (CliffordAlgebraComplex.ofComplex c)
-- Batteries.Lean.Position
/-- Converts a `DeclarationRange` to a `Syntax.Range`. This assumes that the
`DeclarationRange` is sourced in the given `FileMap`.  -/
Lean.DeclarationRange.toSyntaxRange : Lean.FileMap → Lean.DeclarationRange → Lean.Syntax.Range
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ιTotalOrZero.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂),
  K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂ = K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂
-- Init.Internal.Order.Basic
Lean.Order.admissible_flatOrder : ∀ {α : Sort u} {b : α} (P : Lean.Order.FlatOrder b → Prop), P (Lean.Order.FlatOrder.mk b b) → Lean.Order.admissible P
-- Mathlib.Data.List.Basic
List.eq_cons_of_length_one : ∀ {α : Type u} {l : List α} (h : l.length = 1), l = [l.get ⟨0, ⋯⟩]
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_rightUnitor_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c}
  (h : CategoryTheory.CategoryStruct.comp f g ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).hom) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).hom h)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termL₂_1 : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.isIso_cyclesMap_of_isIso_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃]
  [inst_4 : S₁.HasLeftHomology] [inst_5 : S₂.HasLeftHomology],
  CategoryTheory.IsIso (CategoryTheory.ShortComplex.cyclesMap φ)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.mk_zsmul : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) (n : ℤ), ↑(n • a) = n • ↑a
-- Init.Data.Int.Order
Int.natAbs_ofNat' : ∀ (n : ℕ), (Int.ofNat n).natAbs = n
-- Mathlib.Order.BourbakiWitt
/-- If `y` is an extreme point and `f` is inflationary, then there are no element between `y` and
`f y`.  -/
ChainCompletePartialOrder.IsExtremePt.bot_eq_of_le_or_map_le : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α} {y : α},
  (∀ (x : α), x ≤ f x) →
    ChainCompletePartialOrder.IsExtremePt x f y →
      {z | z ∈ ChainCompletePartialOrder.bot x f ∧ (z ≤ y ∨ f y ≤ z)} = ChainCompletePartialOrder.bot x f
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.le_iInf₂_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_4} {ι' : ι → Sort u_5}
  (f : (i : ι) → ι' i → α → ENNReal), ∫⁻ (a : α), ⨅ i, ⨅ h, f i h a ∂μ ≤ ⨅ i, ⨅ h, ∫⁻ (a : α), f i h a ∂μ
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (y : ↥M) (n : ℕ),
  IsLocalization.mk' S (x ^ n) (y ^ n) = IsLocalization.mk' S x y ^ n
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The morphism from a seminormed group to the quotient by a subgroup.  -/
AddSubgroup.normedMk : {M : Type u_1} → [inst : SeminormedAddCommGroup M] → (S : AddSubgroup M) → NormedAddGroupHom M (M ⧸ S)
-- Mathlib.Topology.EMetricSpace.Lipschitz
continuous_prod_of_continuous_lipschitzWith' : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] (f : α × β → γ) (K : NNReal),
  (∀ (a : α), LipschitzWith K fun y => f (a, y)) → (∀ (b : β), Continuous fun x => f (x, b)) → Continuous f
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressBegin.toWorkDoneProgressReport : Lean.Lsp.WorkDoneProgressBegin → Lean.Lsp.WorkDoneProgressReport
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.CharRole.separator : Lean.FuzzyMatching.CharRole
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- The partition of exactly one part.  -/
Nat.Partition.indiscrete : (n : ℕ) → n.Partition
-- Init.Data.Slice.Array.Lemmas
Array.toArray_mkSlice_roo : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...hi) = xs.extract (lo + 1) hi
-- Std.Net.Addr
Std.Net.instDecidableEqIPv6Addr : DecidableEq Std.Net.IPv6Addr
-- Lean.Declaration
Lean.Declaration.opaqueDecl : Lean.OpaqueVal → Lean.Declaration
-- Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
RCLike.measurable_ofReal : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜], Measurable RCLike.ofReal
-- Init.Data.String.Substring
/-- Returns the position that's the specified number of characters prior to the given position in a
substring. If the start position of the substring is reached, it is returned.

Both the input position and the returned position are interpreted relative to the substring's start
position, not the underlying string.
 -/
Substring.Raw.prevn : Substring.Raw → ℕ → String.Pos.Raw → String.Pos.Raw
-- Batteries.Data.PairingHeap
_private.Batteries.Data.PairingHeap.0.Batteries.PairingHeapImp.Heap.combine.match_1.eq_2 : ∀ {α : Type u_1} (motive : Batteries.PairingHeapImp.Heap α → Sort u_2) (h : Batteries.PairingHeapImp.Heap α)
  (h_1 :
    (h₁ : Batteries.PairingHeapImp.Heap α) →
      (a : α) →
        (child h₂ : Batteries.PairingHeapImp.Heap α) →
          (a_1 : α) →
            (child_1 s : Batteries.PairingHeapImp.Heap α) →
              h₂ = Batteries.PairingHeapImp.Heap.node a_1 child_1 s →
                h₁ = Batteries.PairingHeapImp.Heap.node a child (Batteries.PairingHeapImp.Heap.node a_1 child_1 s) →
                  motive
                    (Batteries.PairingHeapImp.Heap.node a child (Batteries.PairingHeapImp.Heap.node a_1 child_1 s)))
  (h_2 : (h : Batteries.PairingHeapImp.Heap α) → motive h),
  (∀ (a : α) (child : Batteries.PairingHeapImp.Heap α) (a_1 : α) (child_1 s : Batteries.PairingHeapImp.Heap α),
      h = Batteries.PairingHeapImp.Heap.node a child (Batteries.PairingHeapImp.Heap.node a_1 child_1 s) → False) →
    (match h with
      | h₁@h_3:(Batteries.PairingHeapImp.Heap.node a child h₂@h:(Batteries.PairingHeapImp.Heap.node a_1 child_1 s)) =>
        h_1 h₁ a child h₂ a_1 child_1 s h h_3
      | h => h_2 h) =
      h_2 h
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_roo : ∀ {m n : ℤ} {i : ℕ}, (m<...n).toArray[i]? = if i < (n - (m + 1)).toNat then some (m + 1 + ↑i) else none
-- Mathlib.Algebra.Group.Prod
/-- The monoid equivalence between units of a product of two monoids, and the product of the
units of each monoid.  -/
MulEquiv.prodUnits : {M : Type u_3} → {N : Type u_4} → [inst : Monoid M] → [inst_1 : Monoid N] → (M × N)ˣ ≃* Mˣ × Nˣ
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.instBEqErrorContext : BEq Mathlib.Linter.TextBased.ErrorContext✝
-- Mathlib.Order.Interval.Multiset
Multiset.mem_Ico : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α}, x ∈ Multiset.Ico a b ↔ a ≤ x ∧ x < b
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ₀Iter_succ : ∀ (i : ℕ) {n m : ℕ} (h : n + (i + 1) = m),
  SimplexCategory.σ₀Iter (i + 1) h =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter i ⋯) (SimplexCategory.σ 0)
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.ofLinearEquiv_symm_of : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsAdicComplete I M] (x : M), (AdicCompletion.ofLinearEquiv I M).symm ((AdicCompletion.of I M) x) = x
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
ContDiffWithinAt.rpow_const_of_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} {p : ℝ}
  {m : ℕ}, ContDiffWithinAt ℝ (↑m) f s x → ↑m ≤ p → ContDiffWithinAt ℝ (↑m) (fun x => f x ^ p) s x
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntInt32SintOfNatNat : Lean.Grind.ToInt Int32 (Lean.Grind.IntInterval.sint 32)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.instNeZeroOne : NeZero 1
-- Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Set.Nonempty.zero_div : ∀ {α : Type u_1} [inst : GroupWithZero α] {s : Set α}, s.Nonempty → 0 / s = 0
-- Mathlib.RingTheory.Valuation.Integers
Valuation.mem_ltSubmodule_iff : ∀ {R : Type u} {Γ₀ : Type v} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {γ : Γ₀ˣ}
  {x : R}, x ∈ v.ltSubmodule γ ↔ v x < ↑γ
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace : ∀ {X : Type u_3} [self : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace X], CompleteSpace X
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_rankFinite : ∀ {α : Type u_1} {M : Matroid α} {D : Set α} [M.RankFinite], (M.delete D).RankFinite
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.FiniteMeasure.normalize.congr_simp : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} (μ μ_1 : MeasureTheory.FiniteMeasure Ω),
  μ = μ_1 → μ.normalize = μ_1.normalize
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- A discrete space `M` is a smooth manifold over the trivial model on a trivial normed space.  -/
IsManifold.of_discreteTopology : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (n : WithTop ℕ∞) {M : Type u_4} [inst_3 : TopologicalSpace M] [inst_4 : DiscreteTopology M]
  [inst_5 : Unique E], IsManifold (modelWithCornersSelf 𝕜 E) n M
-- Mathlib.Data.ENNReal.Operations
ENNReal.le_of_add_le_add_left : ∀ {a b c : ENNReal}, a ≠ ⊤ → a + b ≤ a + c → b ≤ c
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_sub : ∀ (a b : BitVec 8), { toBitVec := a - b } = { toBitVec := a } - { toBitVec := b }
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- the projection from cycles to the (left) homology  -/
CategoryTheory.ShortComplex.LeftHomologyData.π : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → (self : S.LeftHomologyData) → self.K ⟶ self.H
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.category_comp_left : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {X Y Z : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  (α : CategoryTheory.Limits.CatCospanTransformMorphism X Y) (β : CategoryTheory.Limits.CatCospanTransformMorphism Y Z),
  (CategoryTheory.CategoryStruct.comp α β).left = CategoryTheory.CategoryStruct.comp α.left β.left
-- Mathlib.Algebra.Quaternion
Quaternion.star_mul_eq_coe : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), star a * a = ↑(star a * a).re
-- Init.Data.List.Attach
List.attachWith_eq_nil_iff : ∀ {α : Type u_1} {l : List α} {P : α → Prop} {H : ∀ a ∈ l, P a}, l.attachWith P H = [] ↔ l = []
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.mem_toList_iff_mem : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.Rxc.IsAlwaysFinite α]
  {a : α}, a ∈ r.toList ↔ a ∈ r
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sup : ∀ {X : AlgebraicGeometry.Scheme} (Z Z' : TopologicalSpace.Closeds ↥X),
  AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (Z ⊔ Z') =
    AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal Z ⊓ AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal Z'
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- If `f` is a ring seminorm on `a`, then `∀ {n : ℕ}, n ≠ 0 → f (a ^ n) ≤ f a ^ n`.  -/
map_pow_le_pow : ∀ {F : Type u_2} {α : Type u_3} [inst : Ring α] [inst_1 : FunLike F α ℝ] [RingSeminormClass F α ℝ] (f : F) (a : α)
  {n : ℕ}, n ≠ 0 → f (a ^ n) ≤ f a ^ n
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.unit.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a),
  h.unit = (Classical.choose h).copy a ⋯ ↑(Classical.choose h)⁻¹ ⋯
-- Mathlib.Computability.Primrec.Basic
Primcodable.fin : {n : ℕ} → Primcodable (Fin n)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  {f : β → β}, (t.modify k f)[k']? = if cmp k k' = Ordering.eq then Option.map f t[k]? else t[k']?
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.InnerRegular.neg : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [ContinuousNeg G] [μ.InnerRegular], μ.neg.InnerRegular
-- Mathlib.Data.ZMod.Basic
ZMod.cast_id : ∀ (n : ℕ) (i : ZMod n), i.cast = i
-- Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
/-- The yoneda embedding of `TopCat` precomposed with the forgetful functor from `Scheme`. This is the
presheaf `U ↦ C(U, T)`. For universe reasons, we implement it by hand.
 -/
AlgebraicGeometry.continuousMapPresheaf : (T : Type v) → [TopologicalSpace T] → CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ (Type (max v u))
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.image_ball : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (x : α) (r : ℝ),
  ⇑h '' Metric.ball x r = Metric.ball (h x) r
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.isOrderedCommRing : Lean.Meta.Grind.Arith.Linear.LinearM Bool
-- Init.Data.Option.Lemmas
Option.elim_join : ∀ {α : Type u_1} {β : Sort u_2} {o : Option (Option α)} {b : β} {f : α → β},
  o.join.elim b f = o.elim b fun x => x.elim b f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_inj : ∀ {x y : ℝ}, -1 ≤ x → x ≤ 1 → -1 ≤ y → y ≤ 1 → (Real.arcsin x = Real.arcsin y ↔ x = y)
-- Lean.Meta.CoeAttr
Lean.Meta.CoeFnType.coe.sizeOf_spec : sizeOf Lean.Meta.CoeFnType.coe = 1
-- Lean.Hygiene
Lean.Unhygienic.run : {α : Type} → Lean.Unhygienic α → α
-- Mathlib.Algebra.GCDMonoid.Basic
/-- The LCM is normalized to itself.  -/
StrongNormalizedGCDMonoid.normalize_lcm : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : StrongNormalizedGCDMonoid α] (a b : α),
  normalize (lcm a b) = lcm a b
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonUInt64 : Lean.ToJson UInt64
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.lift_apply : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (F : Multiplicative M →* A) (f : AddMonoidAlgebra R M),
  ((AddMonoidAlgebra.lift R A M) F) f = f.coeff.sum fun a b => b • F (Multiplicative.ofAdd a)
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
/-- The unique fixed point of an orientation-preserving elliptic matrix acting on `ℍ`.  -/
UpperHalfPlane.fixedPt : (g : GL (Fin 2) ℝ) → g.IsElliptic → UpperHalfPlane
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left)
  {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (i : J.R),
  CategoryTheory.CategoryStruct.comp (I.sndPiMapOfIsLimit c hd) (d.proj i) =
    CategoryTheory.CategoryStruct.comp (c.proj (J.snd i)) (I.snd i)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesLimitsOfShape_iff_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {F G : CategoryTheory.Functor C D} (h : F ≅ G),
  CategoryTheory.Limits.PreservesLimitsOfShape J F ↔ CategoryTheory.Limits.PreservesLimitsOfShape J G
-- Mathlib.MeasureTheory.Function.LpSeminorm.Count
MeasureTheory.eLpNorm_dirac : ∀ {α : Type u_1} {ε : Type u_2} [inst : MeasurableSpace α] [MeasurableSingletonClass α] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {p : ENNReal} (f : α → ε) (i : α),
  p ≠ 0 → MeasureTheory.eLpNorm f p (MeasureTheory.Measure.dirac i) = ‖f i‖ₑ
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.StrictMono.lift.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {a : ℕ → ℕ} (ha : StrictMono a)
  (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m)
  [inst_5 : IsAdicComplete I N],
  IsAdicComplete.StrictMono.lift I ha f hf = IsAdicComplete.lift I (IsAdicComplete.StrictMono.extend ha f) ⋯
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.to_single_hom_ext : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] {c : ComplexShape ι}
  {K : HomologicalComplex V c} {j : ι} {A : V} {f g : K ⟶ (HomologicalComplex.single V c j).obj A},
  f.f j = g.f j → f = g
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_mul_right : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
  c ≠ 0 → ∫ (x : ℝ) in a..b, f (x * c) = c⁻¹ • ∫ (x : ℝ) in a * c..b * c, f x
-- Mathlib.GroupTheory.Exponent
Monoid.exists_orderOf_eq_exponent : ∀ {G : Type u} [inst : CommMonoid G], Monoid.ExponentExists G → ∃ g, orderOf g = Monoid.exponent G
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientAddGroup.le_norm_iff : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M} {x : M ⧸ S} {r : ℝ},
  r ≤ ‖x‖ ↔ ∀ (m : M), ↑m = x → r ≤ ‖m‖
-- Init.Data.Array.Lemmas
Array.foldl_append : ∀ {α : Type u_1} {β : Type u_2} {f : β → α → β} {b : β} {xs ys : Array α},
  Array.foldl f b (xs ++ ys) = Array.foldl f (Array.foldl f b xs) ys
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.map_comp : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid N']
  [inst_8 : Module R N] [inst_9 : Module R N'] (g : N →ₗ[R] N') [inst_10 : IsLocalizedModule S g] (h : M →ₗ[R] N),
  (IsLocalizedModule.map S f g) h ∘ₗ f = g ∘ₗ h
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_succ_of_mono : ∀ {o : Ordinal.{u_3}} {f : (a : Ordinal.{u_3}) → a < Order.succ o → Ordinal.{max u_3 u_4}},
  (∀ {i j : Ordinal.{u_3}} (hi : i < Order.succ o) (hj : j < Order.succ o), i ≤ j → f i hi ≤ f j hj) →
    (Order.succ o).bsup f = f o ⋯