mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Order
Int.le_add_of_sub_right_le : ∀ {a b c : ℤ}, a - c ≤ b → a ≤ b + c
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.unzeroD_le_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithZero α} {a b : α}, (x = 0 → a ≤ b) → (WithZero.unzeroD a x ≤ b ↔ x ≤ ↑b)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.emptyWithCapacity_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [EquivBEq α] [LawfulHashable α] {c : ℕ},
  Std.ExtDHashMap.emptyWithCapacity c = ∅
-- Mathlib.RingTheory.KrullDimension.Basic
/-- If `R` and `S` are isomorphic, then `ringKrullDim R = ringKrullDim S`.  -/
ringKrullDim_eq_of_ringEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (e : R ≃+* S),
  ringKrullDim R = ringKrullDim S
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.beq_not_ite' : ∀ {a b c : Bool}, (a == !bif c then b else a) = (c && a == !b)
-- Mathlib.Data.Matrix.Block
Matrix.toBlock_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_12} (M : Matrix m n α) (p : m → Prop) (q : n → Prop) (i : { a // p a })
  (j : { a // q a }), M.toBlock p q i j = M ↑i ↑j
-- Mathlib.Analysis.Calculus.Deriv.Star
derivWithin.star : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace 𝕜 F] [inst_4 : StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} {x : 𝕜}
  [TrivialStar 𝕜] {s : Set 𝕜}, derivWithin (fun y => star (f y)) s x = star (derivWithin f s x)
-- Mathlib.NumberTheory.NumberField.Basic
/-- Given an algebra structure between two fields, this instance creates an algebra structure
between their two rings of integers.  -/
NumberField.inst_ringOfIntegersAlgebra : (K : Type u_1) →
  (L : Type u_2) →
    [inst : Field K] →
      [inst_1 : Field L] → [Algebra K L] → Algebra (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.edgeDensity_add_edgeDensity_compl : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {s t : Finset α} [inst_1 : DecidableEq α],
  s.Nonempty → t.Nonempty → Disjoint s t → G.edgeDensity s t + Gᶜ.edgeDensity s t = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k a : α} {v : β k}, a ∈ Std.DTreeMap.Internal.Impl.insertIfNew! k v t ↔ compare k a = Ordering.eq ∨ a ∈ t
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
MeasureTheory.inducedFamily.eq_1 : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (μ : (n : ℕ) → MeasureTheory.Measure ((i : ↥(Finset.Iic n)) → X ↑i)) (S : Finset ℕ),
  MeasureTheory.inducedFamily μ S = MeasureTheory.Measure.map (Finset.restrict₂ ⋯) (μ (S.sup id))
-- Mathlib.Topology.UniformSpace.Pi
Pi.uniformity : ∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)],
  uniformity ((i : ι) → α i) = ⨅ i, Filter.comap (fun a => (a.1 i, a.2 i)) (uniformity (α i))
-- Mathlib.Order.Filter.IndicatorFunction
Filter.EventuallyEq.support : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β] {f g : α → β} {l : Filter α},
  f =ᶠ[l] g → Function.support f =ᶠ[l] Function.support g
-- Init.Data.Float.Model.Format.Basic
/-- Suppose we have written a number where `totalExponent` is the position of the
most significant digit, where the unit digit corresponds to `1`. So, for example,
`1.0b` has total exponent `1`, `0.1b` has total exponent `0`, `0.01b` has total
exponent `-1`, and so on. This function computes which exponent that number
should have according to the given `Format`. So, for example, for the number
`0.1b` in `binary64` format, it wants us to use the exponent `-53`, corresponding
to the representation `2^52 * 2^(-53)`, which has a 53-bit mantissa. If the total
exponent gets quite small, then the result exponent eventually gets capped at
`spec.minExponent`, which first forces the result to be a subnormal number and
then, if the total exponent is even smaller, to be zero.
 -/
Float.Model.Format.targetExponent : Float.Model.Format → ℤ → ℤ
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_toReal_eq : ∀ {α : Type u_1} {f : α → ENNReal}, (∀ (a : α), f a ≠ ⊤) → (∑' (a : α), f a).toReal = ∑' (a : α), (f a).toReal
-- Mathlib.RepresentationTheory.Intertwining
/-- Equivalence between representations induced from `TensorProduct.comm`.  -/
Representation.TensorProduct.comm : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : CommSemiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → (ρ.tprod σ).Equiv (σ.tprod ρ)
-- Std.Do.Internal.Ensures.Lemmas
/-- Compose `Ensures`-witnesses across a monadic bind.  -/
Std.Do.Internal.Ensures.bind : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {α β : Type u} {x : m α} {P : α → Prop} {k : α → m β}
  {Q : β → Prop},
  Std.Do.Internal.Ensures P x → (∀ (a : α), P a → Std.Do.Internal.Ensures Q (k a)) → Std.Do.Internal.Ensures Q (x >>= k)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.pow_nonneg : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : A},
  autoParam (0 ≤ a) CStarAlgebra.pow_nonneg._auto_1 → ∀ (n : ℕ), 0 ≤ a ^ n
-- Mathlib.Probability.ProductMeasure
/-- The `projectiveFamilyContent` associated to a family of probability measures is
σ-subadditive.  -/
MeasureTheory.isSigmaSubadditive_piContent : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)], (MeasureTheory.piContent μ).IsSigmaSubadditive
-- Mathlib.Logic.IsEmpty.Basic
wellFounded_of_isEmpty : ∀ {α : Sort u_4} [IsEmpty α] (r : α → α → Prop), WellFounded r
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.norm_image_zero_le : ∀ {𝕜 : Type u_1} {V : Type u_3} {W : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 V] [inst_4 : NormedSpace 𝕜 W] (f : V →ᴬ[𝕜] W),
  ‖f 0‖ ≤ ‖f‖
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.checkInductionTargets : Array Lean.Expr → Lean.MetaM Unit
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.comp_assoc : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B]
  [inst_3 : Star B] [inst_4 : Monoid C] [inst_5 : Star C] [inst_6 : Monoid D] [inst_7 : Star D] (f : C →⋆* D)
  (g : B →⋆* C) (h : A →⋆* B), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.hasCoeffs : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] (D : Algebra.Smooth.DescentAux✝ A B),
  (Algebra.Smooth.DescentAux.P✝ D).HasCoeffs ↥(Algebra.Smooth.DescentAux.subalgebra✝ R D)
-- Mathlib.Analysis.RCLike.Basic
IsSelfAdjoint.I_smul_of_mem_skewAdjoint : ∀ {K : Type u_1} [inst : RCLike K] {A : Type u_3} [inst_1 : AddCommGroup A] [inst_2 : StarAddMonoid A]
  [inst_3 : Module K A] [StarModule K A] {a : A}, a ∈ skewAdjoint A → IsSelfAdjoint (RCLike.I • a)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.reindex.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  (s : CategoryTheory.Limits.WidePullbackCone f) {ι' : Type u_3} (e : ι' ≃ ι),
  s.reindex e = CategoryTheory.Limits.WidePullbackCone.mk s.base (fun i => s.π (e i)) ⋯
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
/-- The derivative of `compContinuousLinearMap` can be represented
in terms of `alternatizeUncurryFinCLM`.  -/
ContinuousAlternatingMap.fderivCompContinuousLinearMap_eq_alternatizeUncurryFin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ} (f : F [⋀^Fin (n + 1)]→L[𝕜] G) (g : E →L[𝕜] F),
  f.fderivCompContinuousLinearMap g =
    ContinuousAlternatingMap.alternatizeUncurryFinCLM 𝕜 E G ∘SL
      ContinuousLinearMap.postcomp E (ContinuousAlternatingMap.compContinuousLinearMapCLM g ∘SL f.curryLeft)
-- Mathlib.Order.WithBot
WithTop.decidableEq.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α], WithTop.decidableEq = WithTop.decidableEq._aux_1
-- Mathlib.Combinatorics.SimpleGraph.Circulant
/-- Circulant graph over additive group `G` with jumps `s`  -/
SimpleGraph.circulantGraph : {G : Type u_1} → [AddGroup G] → Set G → SimpleGraph G
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.instIsQuasicoherentOfIsLocallyFree : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) [h : M.IsLocallyFree],
  M.IsQuasicoherent
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.cooper_left_core : ∀ {a b p q x : ℤ},
  a < 0 →
    0 < b →
      a * x + p ≤ 0 →
        b * x + q ≤ 0 → Int.Internal.Linear.OrOver a.natAbs fun k => b * p + -a * q + b * ↑k ≤ 0 ∧ a ∣ p + ↑k
-- Mathlib.Topology.Closure
mem_closure_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X},
  x ∈ closure s ↔ ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty
-- Aesop.Forward.RuleInfo
/-- 0-based index of the premise represented by this slot in the rule type.
Note that the slots array may use a different ordering than the original
order of premises, so we *don't* always have `index ≤ premiseIndex`. Rule
pattern slots are assigned an arbitrary premise index.  -/
Aesop.Slot.premiseIndex : Aesop.Slot → Aesop.PremiseIndex
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get!_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], (t₁ ∪ t₂).get! k = t₂.getD k (t₁.get! k)
-- Mathlib.CategoryTheory.Sites.Closed
/-- Being `J`-closed is stable under pullback.  -/
CategoryTheory.GrothendieckTopology.isClosed_pullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X Y : C}
  (f : Y ⟶ X) (S : CategoryTheory.Sieve X), J₁.IsClosed S → J₁.IsClosed (CategoryTheory.Sieve.pullback f S)
-- Mathlib.Order.Hom.Basic
OrderEmbedding.gtEmbedding.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β),
  f.gtEmbedding = { toEmbedding := { toEmbedding := f.toEmbedding, map_rel_iff' := ⋯ }.toEmbedding, map_rel_iff' := ⋯ }
-- Mathlib.RingTheory.Valuation.Discrete.RankOne
Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt.congr_simp : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [inst_1 : Ring R] (v : Valuation R Γ)
  [hv : v.IsRankOneDiscrete],
  Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt v =
    Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt v
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.maxKey! =
    t.maxKey?.elim k fun k' => if (compare k' k).isLE = true then k else k'
-- Init.Omega.IntList
Lean.Omega.IntList.neg_cons : ∀ {x : ℤ} {xs : List ℤ}, -(x :: xs) = -x :: -xs
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.FinValue.mk.inj : ∀ {n : ℕ} {val : Fin n} {n_1 : ℕ} {val_1 : Fin n_1},
  { n := n, val := val } = { n := n_1, val := val_1 } → n = n_1 ∧ val ≍ val_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
/-- `Real.cos` as an `OpenPartialHomeomorph` between `(0, π)` and `(-1, 1)`.  -/
Real.cosPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.sub_neg_of_lt : ∀ {α : Type u} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {a b : α}, a < b → a - b < 0
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_skyscraperPresheafHomEquiv_symm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (g : P ⟶ Φ.skyscraperPresheaf M) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P)
      (CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv.symm g) h) =
    CategoryTheory.CategoryStruct.comp (g.app (Opposite.op X))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun t => M) x) h)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.instHasRightCalculusOfFractionsUnopOfHasLeftCalculusOfFractionsOpposite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ)
  [h : W.HasLeftCalculusOfFractions], W.unop.HasRightCalculusOfFractions
-- Mathlib.Algebra.BigOperators.Field
Multiset.sum_map_div : ∀ {ι : Type u_1} {K : Type u_2} [inst : DivisionSemiring K] (s : Multiset ι) (f : ι → K) (a : K),
  (Multiset.map (fun x => f x / a) s).sum = (Multiset.map f s).sum / a
-- Mathlib.Data.Nat.Log
Nat.log_le_self : ∀ (b x : ℕ), Nat.log b x ≤ x
-- Mathlib.Probability.Distributions.Fernique
ContinuousLinearMap.rotation_apply : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (θ : ℝ) (x : E × E),
  (ContinuousLinearMap.rotation θ) x = (Real.cos θ • x.1 + Real.sin θ • x.2, -Real.sin θ • x.1 + Real.cos θ • x.2)
-- Mathlib.Data.Fintype.Card
Fintype.card_subtype_true : ∀ {α : Type u_1} [inst : Fintype α] {h : Fintype { _a // True }}, Fintype.card { _a // True } = Fintype.card α
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.top_pow : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MonoidWithZero α] [inst_2 : NoZeroDivisors α] [inst_3 : Nontrivial α]
  {n : ℕ}, n ≠ 0 → ⊤ ^ n = ⊤
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- Every entry of a doubly stochastic matrix is nonnegative.  -/
nonneg_of_mem_doublyStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ doublyStochastic R n → ∀ {i j : n}, 0 ≤ M i j
-- Mathlib.Data.Sum.Basic
Sum.update_elim_inr : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq β] [inst_1 : DecidableEq (α ⊕ β)] {f : α → γ} {g : β → γ}
  {i : β} {x : γ}, Function.update (Sum.elim f g) (Sum.inr i) x = Sum.elim f (Function.update g i x)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.readyForRatAdd_delete : ∀ {α : outParam (Type u)} {β : outParam (Type v)} {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w}
  {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (f : σ) (arr : Array ℕ),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f →
    Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f arr)
-- Mathlib.Topology.Inseparable
SeparationQuotient.preimage_mk_frontier : ∀ {X : Type u_1} [inst : TopologicalSpace X] {t : Set (SeparationQuotient X)},
  SeparationQuotient.mk ⁻¹' frontier t = frontier (SeparationQuotient.mk ⁻¹' t)
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.isInducing_mk : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsInducing ⇑DomMulAct.mk
-- Init.Data.List.TakeDrop
List.ne_nil_of_take_ne_nil : ∀ {α : Type u_1} {as : List α} {i : ℕ}, List.take i as ≠ [] → as ≠ []
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.instAddCommMonoidOreLocalization : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} →
          [inst_2 : AddCommMonoid X] → [inst_3 : DistribMulAction R X] → AddCommMonoid (OreLocalization S X)
-- Mathlib.RingTheory.Unramified.LocalRing
Algebra.instFiniteResidueFieldOfIsUnramifiedAt : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.EssFiniteType R S] (p : Ideal R) [inst_4 : p.IsPrime] (q : Ideal S) [inst_5 : q.IsPrime]
  [inst_6 : q.LiesOver p] [inst_7 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
  [inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q] [Algebra.IsUnramifiedAt R q],
  Module.Finite p.ResidueField q.ResidueField
-- Aesop.Forward.Match.Types
/-- A match associates hypotheses to (a prefix of) the slots of a slot
cluster.  -/
Aesop.Match : Type
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.instSubsingletonOfForall : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Subsingleton (V → W)], Subsingleton (G →g H)
-- Mathlib.Order.BooleanAlgebra.Set
Set.subset_compl_singleton_iff : ∀ {α : Type u_1} {s : Set α} {a : α}, s ⊆ {a}ᶜ ↔ a ∉ s
-- Mathlib.Data.Nat.Cast.Order.Field
Nat.one_div_cast_ne_zero : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {n : ℕ}, n ≠ 0 → 1 / ↑n ≠ 0
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterMap.match_1.splitter : {γ : Type u_1} →
  (motive : Option γ → Sort u_2) →
    (x : Option γ) → (x = none → motive none) → ((out' : γ) → x = some out' → motive (some out')) → motive x
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonianCycle.support_count_of_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a a},
  p.IsHamiltonianCycle → a ≠ b → List.count b p.support = 1
-- Mathlib.LinearAlgebra.Multilinear.Pi
/-- Given a family of indices `κ` and a multilinear map `f p` for each way `p` to select one index from
each family, `piFamily f` maps a family of functions (one for each domain `κ i`) into a function
from each selection of indices (with domain `Π i, κ i`).
 -/
MultilinearMap.piFamily : {ι : Type uι} →
  {κ : ι → Type uκ} →
    {R : Type uR} →
      {M : (i : ι) → κ i → Type uM} →
        {N : ((i : ι) → κ i) → Type uN} →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] →
              [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] →
                [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)] →
                  [inst_4 : (p : (i : ι) → κ i) → Module R (N p)] →
                    ((p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)) →
                      MultilinearMap R (fun i => (j : κ i) → M i j) ((t : (i : ι) → κ i) → N t)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.wf_insertMany₀ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w}
  [inst_4 : ForIn Id ρ (α × β)] {m : Std.DHashMap.Raw α fun x => β} {h : 0 < m.buckets.size} {l : ρ},
  m.WF → (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany ⟨m, h⟩ l)).WF
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isNClique_zero : ∀ {α : Type u_1} {G : SimpleGraph α} {s : Finset α}, G.IsNClique 0 s ↔ s = ∅
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.over_def : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens), ↑U ↘ X = U.ι
-- Init.Data.PLift
instDecidableEqPLift : {α : Sort u_1} → [DecidableEq α] → DecidableEq (PLift α)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeGPFree.instDecidable.eq_1 : ∀ {α : Type u_2} [inst : Monoid α] [inst_1 : DecidableEq α] {s : Finset α},
  ThreeGPFree.instDecidable = decidable_of_iff (∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, a * c = b * b → a = b) ⋯
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
argSelfAdjoint_expUnitary : ∀ {A : Type u_1} [inst : CStarAlgebra A] {x : ↥(selfAdjoint A)},
  ‖x‖ < Real.pi → Unitary.argSelfAdjoint (selfAdjoint.expUnitary x) = x
-- Mathlib.Algebra.BigOperators.Module
_private.Mathlib.Algebra.BigOperators.Module.0.Finset.termG_ : Lean.ParserDescr
-- Init.Data.List.Nat.Perm
List.set_set_perm : ∀ {α : Type u_1} {as : List α} {i j : ℕ} (h₁ : i < as.length) (h₂ : j < as.length),
  ((as.set i as[j]).set j as[i]).Perm as
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.apply_eq_self_iff : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → (f x = x ↔ f y = y)
-- Mathlib.Topology.LocallyConstant.Basic
/-- The constant locally constant function on `X` with value `y : Y`.  -/
LocallyConstant.const : (X : Type u_5) → {Y : Type u_6} → [inst : TopologicalSpace X] → Y → LocallyConstant X Y
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.id_apply : ∀ (M : Type u_10) [inst : MulOne M] (x : M), (MonoidHom.id M) x = x
-- Mathlib.Probability.Kernel.Posterior
/-- The posterior of the identity kernel is the identity kernel.  -/
ProbabilityTheory.posterior_id : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] [inst_1 : Nonempty Ω]
  (μ : MeasureTheory.Measure Ω) [inst_2 : MeasureTheory.IsFiniteMeasure μ],
  ⇑(ProbabilityTheory.posterior ProbabilityTheory.Kernel.id μ) =ᵐ[μ] ⇑ProbabilityTheory.Kernel.id
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGT!_eq_get!_getKeyGT? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α} [inst_1 : Inhabited α],
  Std.DTreeMap.Internal.Impl.getKeyGT! k t = (Std.DTreeMap.Internal.Impl.getKeyGT? k t).get!
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.vInv_iso_hom_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] (T : CategoryTheory.Functor C₁ C₂) (L : C₁ ≌ C₃) (R : C₂ ≌ C₄)
  (B : CategoryTheory.Functor C₃ C₄) (x : CategoryTheory.CatCommSq T L.functor R.functor B) (X : C₃),
  (CategoryTheory.CatCommSq.iso B L.inverse R.inverse T).hom.app X =
    CategoryTheory.CategoryStruct.comp (R.inverse.map (B.map (L.counitIso.inv.app X)))
      (CategoryTheory.CategoryStruct.comp
        (R.inverse.map ((CategoryTheory.CatCommSq.iso T L.functor R.functor B).inv.app (L.inverse.obj X)))
        (R.unitIso.inv.app (T.obj (L.inverse.obj X))))
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_one : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R], Matrix.det 1 = 1
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.coe_zero : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N], ⇑0 = 0
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Up to `Scheme.Modules.overEquiv`, `SheafOfModules.overMap` is isomorphic to
`Scheme.Modules.restrictFunctor`.  -/
AlgebraicGeometry.Scheme.Modules.overMapCompOverEquiv : {X : AlgebraicGeometry.Scheme} →
  {U V : X.Opens} →
    (f : V ⟶ U) →
      (SheafOfModules.overMap X.ringCatSheaf f).comp (AlgebraicGeometry.Scheme.Modules.overEquiv V).functor ≅
        (AlgebraicGeometry.Scheme.Modules.overEquiv U).functor.comp
          (AlgebraicGeometry.Scheme.Modules.restrictFunctor (X.homOfLE ⋯))