mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Category.Basic
/-- The typeclass `Category C` describes morphisms associated to objects of type `C : Type u`.

The universe levels of the objects and morphisms are independent, and will often need to be
specified explicitly, as `Category.{v} C`.

Typically any concrete example will either be a `SmallCategory`, where `v = u`,
which can be introduced as
```
universe u
variable {C : Type u} [SmallCategory C]
```
or a `LargeCategory`, where `u = v+1`, which can be introduced as
```
universe u
variable {C : Type (u+1)} [LargeCategory C]
```

In order for the library to handle these cases uniformly,
we generally work with the unconstrained `Category.{v u}`,
for which objects live in `Type u` and morphisms live in `Type v`.

Because the universe parameter `u` for the objects can be inferred from `C`
when we write `Category C`, while the universe parameter `v` for the morphisms
cannot be automatically inferred, through the category theory library
we introduce universe parameters with morphism levels listed first,
as in
```
universe v u
```
or
```
universe v₁ v₂ u₁ u₂
```
when multiple independent universes are needed.

This has the effect that we can simply write `Category.{v} C`
(that is, only specifying a single parameter) while `u` will be inferred.

Often, however, it's not even necessary to include the `.{v}`.
(Although it was in earlier versions of Lean.)
If it is omitted a "free" universe will be used.
 -/
LibraryNote.category_theory_universes : Batteries.Util.LibraryNote
-- Mathlib.Data.Finmap
AList.erase.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : AList β),
  AList.erase a s = { entries := List.kerase a s.entries, nodupKeys := ⋯ }
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.map_neg_one : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R ≃+* S), f (-1) = -1
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.RingId.0.Lean.Meta.Grind.Arith.CommRing.getCommSemiringId?.go? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).get k h' = t₂.get k ⋯
-- Lean.Data.SMap
Lean.instReprSMap : {α : Type u_1} → {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → [Repr α] → [Repr β] → Repr (Lean.SMap α β)
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.LaxMonoidalFunctor C D} {α β : F ⟶ G}, α.hom = β.hom → α = β
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_map_sub : ∀ {ι : Type u_2} {G : Type u_4} [inst : SubtractionCommMonoid G] {m : Multiset ι} {f g : ι → G},
  (Multiset.map (fun i => f i - g i) m).sum = (Multiset.map f m).sum - (Multiset.map g m).sum
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_neg : ∀ {R : Type u_1} [inst : Ring R] (x y : R) (p : Polynomial (Polynomial R)),
  Polynomial.evalEval x y (-p) = -Polynomial.evalEval x y p
-- Mathlib.Order.SuccPred.Basic
Order.pred_le_iff_eq_or_le : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α}, Order.pred b ≤ a ↔ a = Order.pred b ∨ b ≤ a
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
summable_pnat_iff_summable_succ : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {f : ℕ → M},
  (Summable fun x => f ↑x) ↔ Summable fun x => f (x + 1)
-- Mathlib.Algebra.Ring.CentroidHom
/-- A prime associative ring has commutative centroid.  -/
CentroidHom.commRing : {α : Type u_5} →
  [inst : NonUnitalRing α] → (∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0) → CommRing (CentroidHom α)
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.fst : ∀ {Ω : Type u_1} {E : Type u_2} {F : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E]
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F] [inst_6 : MeasurableSpace F] {Y : Ω → F},
  ProbabilityTheory.HasGaussianLaw (fun ω => (X ω, Y ω)) P → ProbabilityTheory.HasGaussianLaw X P
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.d₁_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] {i₁ i₁' : ι₁},
  c₁.Rel i₁ i₁' → ∀ (i₂ : ι₂) (i₃ : ι₃) (j : ι₄), ⋯ = ⋯
-- Mathlib.Data.Rat.Cast.CharZero
/-- Coercion `ℚ≥0 → α` as a `RingHom`.  -/
NNRat.castHom : (α : Type u_3) → [inst : DivisionSemiring α] → [CharZero α] → ℚ≥0 →+* α
-- Lean.Server.Completion.CompletionCollectors
/-- Adds a new completion item with the given `label`, `id`, `kind` and `score` to the state in `M`.
Computes the doc string from the environment if available.
 -/
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.addUnresolvedCompletionItem : Lean.Name →
  Lean.Lsp.CompletionIdentifier →
    Lean.Lsp.CompletionItemKind → Array Lean.Lsp.CompletionItemTag → Lean.Server.Completion.M✝ Unit
-- Mathlib.Topology.Compactness.SigmaCompact
instSigmaCompactSpaceForallOfFinite : ∀ {ι : Type u_3} [Finite ι] {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), SigmaCompactSpace (X i)], SigmaCompactSpace ((i : ι) → X i)
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
ordinaryHypergeometricSeries.congr_simp : ∀ {𝕂 : Type u_1} (𝔸 : Type u_2) [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (a a_1 : 𝕂),
  a = a_1 →
    ∀ (b b_1 : 𝕂),
      b = b_1 →
        ∀ (c c_1 : 𝕂),
          c = c_1 → ∀ (n : ℕ), ordinaryHypergeometricSeries 𝔸 a b c n = ordinaryHypergeometricSeries 𝔸 a_1 b_1 c_1 n
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.image_le_image_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U U' : X.Opens),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U ≤ (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U' ↔ U ≤ U'
-- Mathlib.Data.Sign.Defs
/-- The type of signs.  -/
SignType : Type
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.instNormalCenter : ∀ {G : Type u_1} [inst : AddGroup G], (AddSubgroup.center G).Normal
-- Mathlib.RingTheory.AdjoinRoot
AlgEquiv.ofRingEquiv.congr_simp : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {f f_1 : A₁ ≃+* A₂} (e_f : f = f_1)
  (hf : ∀ (x : R), f ((algebraMap R A₁) x) = (algebraMap R A₂) x), AlgEquiv.ofRingEquiv hf = AlgEquiv.ofRingEquiv ⋯
-- Mathlib.Data.List.SplitLengths
List.splitLengths.eq_def : ∀ {α : Type u_1} (x : List ℕ) (x_1 : List α),
  x.splitLengths x_1 =
    match x, x_1 with
    | [], x => []
    | n :: ns, x =>
      match List.splitAt n x with
      | (x0, x1) => x0 :: ns.splitLengths x1
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.snd_δ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃) S.δ =
    CategoryTheory.CategoryStruct.comp S.φ₁ S.v₂₃.τ₁
-- Mathlib.RingTheory.Perfection
/-- For a perfect ring, it itself is the perfection.  -/
PerfectionMap.id : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (R : Type u₁) [inst_1 : CommSemiring R] [inst_2 : CharP R p]
  [inst_3 : PerfectRing R p], PerfectionMap p (RingHom.id R)
-- Mathlib.Data.Multiset.Fold
Multiset.fold_cons_left : ∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b a : α) (s : Multiset α),
  Multiset.fold op b (a ::ₘ s) = op a (Multiset.fold op b s)
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The equivalence of categories `LightProfinite ≌ LightDiagram`  -/
LightProfinite.equivDiagram : LightProfinite ≌ LightDiagram
-- Init.Data.UInt.Lemmas
UInt64.sub_eq_iff_eq_add : ∀ {a b c : UInt64}, a - b = c ↔ a = c + b
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
VectorFourier.fderiv_fourierIntegral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V]
  {μ : MeasureTheory.Measure V},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable (fun v => ‖v‖ * ‖f v‖) μ →
      fderiv ℝ (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f) =
        VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L)
          (VectorFourier.fourierSMulRight L f)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.equivOfIsoObj_symm_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type w)} {X Y : C}
  (e : Y ≅ X) (R : F.CorepresentableBy Y),
  (CategoryTheory.Functor.CorepresentableBy.equivOfIsoObj e).symm R = R.ofIsoObj e.symm
-- Mathlib.Topology.Homeomorph.Defs
HomeomorphClass.coe_coe : ∀ {F : Type u_5} {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : EquivLike F α β] [h : HomeomorphClass F α β] (f : F), ⇑↑f = ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.π_iso_of_iso_left_inv : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ f₁' : CategoryTheory.Arrow C₁}
  {f₃ : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom)
  (iso : f₁ ≅ f₁'), (sq₁₃.π_iso_of_iso_left sq₁₃' iso).inv = sq₁₃'.mapArrowLeft sq₁₃ iso.hom
-- Init.Data.Int.Gcd
Int.lcm_dvd_lcm_mul_right_right : ∀ (a b c : ℤ), a.lcm b ∣ a.lcm (b * c)
-- Mathlib.Analysis.Calculus.FDeriv.Congr
HasFDerivWithinAt.congr' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x → Set.EqOn f₁ f s → x ∈ s → HasFDerivWithinAt f₁ f' s x
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize.match_1.eq_3 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1)
  (h_1 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.threeMore),
  (match ByteArray.utf8DecodeChar?.FirstByte.oneMore with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 ()
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 ()
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 ()
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 ()
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 ()) =
    h_3 ()
-- Mathlib.Analysis.LocallyConvex.AbsConvexOpen
gaugeSeminormFamily_ball : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : Module ℝ E] [inst_5 : IsScalarTower ℝ 𝕜 E] [inst_6 : ContinuousSMul ℝ E]
  (s : AbsConvexOpenSets 𝕜 E), (gaugeSeminormFamily 𝕜 E s).ball 0 1 = ↑s
-- Mathlib.Order.Hom.Lattice
InfHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Min β] (f : α → β) (hf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b),
  ⇑{ toFun := f, map_inf' := hf } = f
-- Init.Data.List.Lemmas
List.lawfulBEq_iff : ∀ {α : Type u_1} [inst : BEq α], LawfulBEq (List α) ↔ LawfulBEq α
-- Mathlib.Algebra.Lie.Ideal
lie_mem_left : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (x y : L), x ∈ I → ⁅x, y⁆ ∈ I
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoc_injective_left : ∀ {α : Type u_1} [inst : LinearOrder α] (a : α), Function.Injective (Set.uIoc a)
-- Mathlib.Algebra.Module.BigOperators
Finset.sum_smul : ∀ {ι : Type u_1} {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f : ι → R} {s : Finset ι} {x : M}, (∑ i ∈ s, f i) • x = ∑ i ∈ s, f i • x
-- Mathlib.Algebra.Order.SuccPred
SuccAddOrder.toSuccOrder : {α : Type u_1} → {inst : Preorder α} → {inst_1 : Add α} → {inst_2 : One α} → [self : SuccAddOrder α] → SuccOrder α
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.ι_obj_lift_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (X : C),
  P.ι.obj ((P.lift F hF).obj X) = F.obj X
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.prod_iff : ∀ {α : Type u_4} {β : Type u_5} [inst : AddMonoid α] [inst_1 : AddMonoid β] {x : α × β},
  IsOfFinAddOrder x ↔ IsOfFinAddOrder x.1 ∧ IsOfFinAddOrder x.2
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.isUnit_iff : ∀ {α : outParam (Type u)} {β : Type v} [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] (c : β)
  (l : Std.Sat.Literal α),
  Std.Tactic.BVDecide.LRAT.Internal.Clause.isUnit c = some l ↔ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c = [l]
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.continuous_CC'₁ : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  Continuous (Profinite.NobelingProof.CC'₁ C hsC ho)
-- Mathlib.Logic.Equiv.Basic
Equiv.eq_conj : ∀ {α : Sort u_11} {α' : Sort u_12} {β : Sort u_13} {β' : Sort u_14} (ε₁ : α ≃ α') (ε₂ : β' ≃ β) (f : α → β)
  (f' : α' → β'), ⇑ε₂.symm ∘ f ∘ ⇑ε₁.symm = f' ↔ f = ⇑ε₂ ∘ f' ∘ ⇑ε₁
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_I₀ : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft 𝒰 f g).I₀ = 𝒰.I₀
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.substAlgHom_coe : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} (ha : MvPowerSeries.HasSubst a) (p : MvPolynomial σ R),
  (MvPowerSeries.substAlgHom ha) ↑p = (MvPolynomial.aeval a) p
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.h1Cotangentι_ext : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (x y : P.H1Cotangent), ↑x = ↑y → x = y
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Returns the next denominator `Bₙ = bₙ₋₁ * Bₙ₋₁ + aₙ₋₁ * Bₙ₋₂`, where `predB` is `Bₙ₋₁` and
`ppredB` is `Bₙ₋₂`, `a` is `aₙ₋₁`, and `b` is `bₙ₋₁`.
 -/
GenContFract.nextDen : {K : Type u_2} → [DivisionRing K] → K → K → K → K → K
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.mul_div_cancel' : ∀ {R : Type u} [inst : EuclideanDomain R] {a b : R}, b ≠ 0 → b ∣ a → b * (a / b) = a
-- Lean.Parser.Term
Lean.Parser.Term.optConfig.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Nat.Bitwise.Lemmas
Nat.or_mod_two_eq_one : ∀ {a b : ℕ}, (a ||| b) % 2 = 1 ↔ a % 2 = 1 ∨ b % 2 = 1
-- Mathlib.Computability.TuringMachine.Tape
Turing.Dir.left.sizeOf_spec : sizeOf Turing.Dir.left = 1
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.SolverExtension.mk.injEq : ∀ {σ : Type} (id : ℕ) (mkInitial : IO σ) (internalize : Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM Unit)
  (newEq newDiseq : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit) (mbtc : Lean.Meta.Grind.GoalM Bool)
  (action : Lean.Meta.Grind.Action) (check : Lean.Meta.Grind.GoalM Bool) (checkInv : Lean.Meta.Grind.GoalM Unit)
  (id_1 : ℕ) (mkInitial_1 : IO σ) (internalize_1 : Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM Unit)
  (newEq_1 newDiseq_1 : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit) (mbtc_1 : Lean.Meta.Grind.GoalM Bool)
  (action_1 : Lean.Meta.Grind.Action) (check_1 : Lean.Meta.Grind.GoalM Bool) (checkInv_1 : Lean.Meta.Grind.GoalM Unit),
  ({ id := id, mkInitial := mkInitial, internalize := internalize, newEq := newEq, newDiseq := newDiseq, mbtc := mbtc,
        action := action, check := check, checkInv := checkInv } =
      { id := id_1, mkInitial := mkInitial_1, internalize := internalize_1, newEq := newEq_1, newDiseq := newDiseq_1,
        mbtc := mbtc_1, action := action_1, check := check_1, checkInv := checkInv_1 }) =
    (id = id_1 ∧
      mkInitial = mkInitial_1 ∧
        internalize = internalize_1 ∧
          newEq = newEq_1 ∧
            newDiseq = newDiseq_1 ∧ mbtc = mbtc_1 ∧ action = action_1 ∧ check = check_1 ∧ checkInv = checkInv_1)
-- Mathlib.Algebra.GroupWithZero.Associated
/-- The quotient of a monoid by the `Associated` relation. Two elements `x` and `y`
are associated iff there is a unit `u` such that `x * u = y`. There is a natural
monoid structure on `Associates M`.  -/
Associates : (M : Type u_2) → [Monoid M] → Type u_2
-- Mathlib.Topology.NhdsWithin
eventually_nhdsWithin_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop},
  (∀ᶠ (x : α) in nhdsWithin a s, p x) ↔ ∀ᶠ (x : α) in nhds a, x ∈ s → p x
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_derivative_mem_span_T : ∀ {R : Type u_1} [inst : CommRing R] (n : ℕ),
  Polynomial.derivative (Polynomial.Chebyshev.T R ↑n) ∈
    Submodule.span ℕ ((fun m => Polynomial.Chebyshev.T R ↑m) '' Set.Ico 0 n)
-- Qq.Macro
/-- Maps free variables in the new context to expressions in the old context (of type Expr)  -/
Qq.Impl.UnquoteState.exprBackSubst : Qq.Impl.UnquoteState → Std.HashMap Lean.Expr Qq.Impl.ExprBackSubstResult
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.Fin.circulant_mul_comm : ∀ {α : Type u_1} [inst : CommMagma α] [inst_1 : AddCommMonoid α] {n : ℕ} (v w : Fin n → α),
  Matrix.circulant v * Matrix.circulant w = Matrix.circulant w * Matrix.circulant v
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.ConnectedComponent.even_card_of_isPerfectMatching : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} [inst : Fintype V] [inst_1 : DecidableEq V]
  [inst_2 : DecidableRel G.Adj] (c : G.ConnectedComponent), M.IsPerfectMatching → Even (Fintype.card ↑c.supp)
-- Mathlib.Algebra.Opposites
MulOpposite.instInvolutiveNeg : {α : Type u_1} → [InvolutiveNeg α] → InvolutiveNeg αᵐᵒᵖ
-- Mathlib.Analysis.Normed.Ring.Basic
/-- The restriction of a power-multiplicative function to a subalgebra is power-multiplicative.  -/
IsPowMul.restriction : ∀ {R : Type u_5} {S : Type u_6} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (A : Subalgebra R S)
  {f : S → ℝ}, IsPowMul f → IsPowMul fun x => f ↑x
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.map_appLE'_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : U' = U) {Z : CommRingCat}
  (h : X.presheaf.obj (Opposite.op V) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom i).op)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U' V ⋯) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U V e) h
-- Aesop.RuleTac.ElabRuleTerm
Aesop.runTacticMAsElabM : {α : Type} → Lean.Elab.Tactic.TacticM α → Aesop.ElabM α
-- Init.Data.Slice.List.Lemmas
List.toList_mkSlice_roc : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  Std.Slice.toList (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = List.drop (lo + 1) (List.take (hi + 1) xs)
-- Init.Data.Option.Lemmas
Option.pfilter_congr : ∀ {α : Type u} {o o' : Option α} (ho : o = o') {f : (a : α) → o = some a → Bool} {g : (a : α) → o' = some a → Bool},
  (∀ (a : α) (ha : o' = some a), f a ⋯ = g a ha) → o.pfilter f = o'.pfilter g
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map : ∀ {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] {G : CategoryTheory.Functor C D} {A : Type w}
  [inst_2 : CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} [inst_3 : G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A}
  (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α : G.op.comp R ⟶ F) {X : D}
  {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y : C} (f : G.obj Y ⟶ X) {W : C} (g : W ⟶ Y)
  (i : S.Arrow) (h : G.obj W ⟶ i.Y),
  CategoryTheory.CategoryStruct.comp h i.f = CategoryTheory.CategoryStruct.comp (G.map g) f →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f) (F.map g.op) =
      CategoryTheory.CategoryStruct.comp (s.ι i)
        (CategoryTheory.CategoryStruct.comp (R.map h.op) (α.app (Opposite.op W)))
-- Mathlib.Order.Types.Defs
/-- An order type lifted to the same universe equals itself.  -/
OrderType.lift_id : ∀ (o : OrderType.{u}), OrderType.lift.{u, u} o = o
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.ofReal_lpNorm : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E},
  MeasureTheory.MemLp f p μ → ENNReal.ofReal (MeasureTheory.lpNorm f p μ) = MeasureTheory.eLpNorm f p μ
-- Init.Data.Array.Attach
Array.pmap_ne_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) {xs : Array α} (H : ∀ a ∈ xs, P a),
  Array.pmap f xs H ≠ #[] ↔ xs ≠ #[]