mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fintype.BigOperators
/-- Product over a sigma type equals the repeated product.

This is a version of `Finset.prod_sigma` specialized to the case
of multiplication over `Finset.univ`.  -/
Fintype.prod_sigma : ∀ {ι : Type u_9} {α : ι → Type u_7} {M : Type u_8} [inst : Fintype ι] [inst_1 : (i : ι) → Fintype (α i)]
  [inst_2 : CommMonoid M] (f : Sigma α → M), ∏ x, f x = ∏ x, ∏ y, f ⟨x, y⟩
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.instHasNoLoopIntDown : (ComplexShape.down ℤ).HasNoLoop
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.List.ProveNilOrConsResult.cons.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(List «$α»)} {a : Q(«$α»)} {s' : Q(List «$α»)} {pf : Q(«$s» = «$a» :: «$s'»)}
  {a_1 : Q(«$α»)} {s'_1 : Q(List «$α»)} {pf_1 : Q(«$s» = «$a_1» :: «$s'_1»)},
  Mathlib.Meta.List.ProveNilOrConsResult.cons a s' pf = Mathlib.Meta.List.ProveNilOrConsResult.cons a_1 s'_1 pf_1 →
    a = a_1 ∧ s' = s'_1 ∧ pf = pf_1
-- Mathlib.Data.String.Basic
String.lt_iff_ltb : ∀ {s₁ s₂ : String}, s₁ < s₂ ↔ String.ltb (String.Legacy.iter s₁) (String.Legacy.iter s₂) = true
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.Offset.ofSeconds.sizeOf_spec : ∀ (second : Std.Time.Second.Offset), sizeOf { second := second } = 1 + sizeOf second
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- The product of the Riemann zeta function with the L-function of `B.χ`.
We will show that `B.F (-2) = 0` but also that `B.F (-2)` must be positive,
giving the desired contradiction.  -/
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar.F : {N : ℕ} → [inst : NeZero N] → DirichletCharacter.BadChar✝ N → ℂ → ℂ
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
exists_linearIndependent : ∀ (K : Type u_3) {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (t : Set V),
  ∃ b ⊆ t, Submodule.span K b = Submodule.span K t ∧ LinearIndependent K Subtype.val
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.isoMk_inv : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} {x : CommRing X} {x_1 : CommRing Y} {x_2 : HopfAlgebra R X}
  {x_3 : HopfAlgebra R Y} (e : X ≃ₐc[R] Y), (CommHopfAlgCat.isoMk e).inv = CommHopfAlgCat.ofHom ↑e.symm
-- Mathlib.Algebra.BigOperators.Ring.Finset
Commute.sum_left : ∀ {ι : Type u_1} {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] (s : Finset ι) (f : ι → R) (b : R),
  (∀ i ∈ s, Commute (f i) b) → Commute (∑ i ∈ s, f i) b
-- Mathlib.RingTheory.Trace.Basic
/-- A family of vectors `v` is the dual for the trace of the basis `b` if and only if
`∀ i j, Tr(v i * b j) = δ_ij`.
 -/
Module.Basis.traceDual_eq_iff : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type w}
  [inst_3 : FiniteDimensional K L] [inst_4 : Algebra.IsSeparable K L] [inst_5 : Finite ι] [inst_6 : DecidableEq ι]
  {b : Module.Basis ι K L} {v : ι → L},
  ⇑b.traceDual = v ↔ ∀ (i j : ι), ((Algebra.traceForm K L) (v i)) (b j) = if j = i then 1 else 0
-- Mathlib.Logic.Equiv.Set
/-- If a function is a bijection between two sets `s` and `t`, then it induces an
equivalence between the types `↥s` and `↥t`.  -/
Set.BijOn.equiv : {α : Type u_1} → {β : Type u_2} → {s : Set α} → {t : Set β} → (f : α → β) → Set.BijOn f s t → ↑s ≃ ↑t
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atom_same : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (a : ℤ), IsEllipticNet.atom W a a = W a * W 0
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.le_liminf_mul : ∀ {ι : Type u_4} {f : Filter ι} {u v : ι → ENNReal}, Filter.liminf u f * Filter.liminf v f ≤ Filter.liminf (u * v) f
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.map_sInf' : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f : α → β},
  RightOrdContinuous f → ∀ {s : Set α}, s.Nonempty → f (sInf s) = sInf (f '' s)
-- Mathlib.Topology.Category.TopCat.Opens
/-- The inclusion `⊥ ⟶ U` as a morphism in the category of open sets.
 -/
TopologicalSpace.Opens.botLE : {X : TopCat} → (U : TopologicalSpace.Opens ↑X) → ⊥ ⟶ U
-- Mathlib.Condensed.Discrete.Colimit
/-- A presheaf `F`, which takes a light profinite set written as a sequential limit to the corresponding
colimit, is isomorphic to the presheaf `LocallyConstant - F(*)`.
 -/
LightCondensed.isoLocallyConstantOfIsColimit : (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) →
  [CategoryTheory.Limits.PreservesFiniteProducts F] →
    ((S : LightProfinite) →
        CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) →
      (F ≅
        LightCondensed.locallyConstantPresheaf
          (F.obj (FintypeCat.toLightProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1})))))
-- Mathlib.Data.Finset.Defs
Finset.decidableExistsAndFinset : {α : Type u_1} → {s : Finset α} → {p : α → Prop} → [_hp : (a : α) → Decidable (p a)] → Decidable (∃ a ∈ s, p a)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToGELT_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : EInt) (X : C),
  (t.eTruncLTGELTSelfToGELT a b).app X = (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X))
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Set.subtype_smul_set : ∀ {S : Type u_7} {α : Type u_8} {β : Type u_9} [inst : SMul α β] [inst_1 : SetLike S α] {s : S} (x : ↥s) (t : Set β),
  x • t = ↑x • t
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_le_comap_iff_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f → ∀ {S T : Submonoid N}, Submonoid.comap f S ≤ Submonoid.comap f T ↔ S ≤ T
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.strictMonoOn_sin : StrictMonoOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
StandardSubspace.ext : ∀ {H : Type u_1} {inst : NormedAddCommGroup H} {inst_1 : InnerProductSpace ℂ H} {x y : StandardSubspace H},
  x.toClosedSubmodule = y.toClosedSubmodule → x = y
-- Std.Data.DHashMap.Raw
/-- Retrieves the key-value pair, whose key matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The key in the returned pair will be `BEq` to the input `a`.
 -/
Std.DHashMap.Raw.getEntry : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → (m : Std.DHashMap.Raw α β) → (a : α) → a ∈ m → (a : α) × β a
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.lt_inducedMap_iff`. -/
LinearOrderedField.lt_inducedMap_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} {b : β},
  b < ConditionallyCompleteLinearOrderedField.inducedMap α β a ↔ ∃ q, b < ↑q ∧ ↑q < a
-- Init.System.CancelToken
/-- Cancellation token for cooperative task cancellation: request cancellation with
`CancelToken.set` and check for it with `CancelToken.isSet`. To react to cancellation without
polling, register a callback with `CancelToken.onSet`.

This is a more flexible alternative to `Task.cancel` as the token can be shared between multiple
tasks.

Note: the underlying `Promise` and the task it produces are kept private. If a future change
exposes the underlying task (or the promise) publicly, the `set` implementation must be
audited for races between resolving the promise and writing `setRef`: callers observing
`isSet = true` and then waiting on the task currently rely on the order chosen in `set`, and
that ordering interacts with the cheap `Bool` fast path read by the C++ runtime.
 -/
IO.CancelToken : Type
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_eq_singleton_iff : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b c : α},
  Finset.Icc a b = {c} ↔ a = c ∧ b = c
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instInhabited.eq_1 : CommGrpCat.instInhabited = { default := CommGrpCat.of PUnit.{u_1 + 1} }
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.applyOrderedFinpartition_update_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (c : OrderedFinpartition n) (p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F) (m : Fin c.length) (v : Fin n → E)
  (q : E [×c.partSize m]→L[𝕜] F),
  c.applyOrderedFinpartition (Function.update p m q) v =
    Function.update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m))
-- Lean.Message
Lean.MessageSeverity.warning : Lean.MessageSeverity
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.instCompScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsIntegralHom f]
  [AlgebraicGeometry.IsIntegralHom g], AlgebraicGeometry.IsIntegralHom (CategoryTheory.CategoryStruct.comp f g)
-- Lean.LocalContext
Lean.LocalDeclKind.ofNat_ctorIdx : ∀ (x : Lean.LocalDeclKind), Lean.LocalDeclKind.ofNat x.ctorIdx = x
-- Mathlib.Algebra.Category.Grp.Basic
mulEquivIsoCommGroupIso.eq_1 : ∀ {X Y : CommGrpCat},
  mulEquivIsoCommGroupIso =
    { hom := TypeCat.ofHom fun e => e.toCommGrpIso, inv := TypeCat.ofHom fun i => i.commGroupIsoToMulEquiv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Data.ENNReal.Inv
ENNReal.ofReal_div_of_pos : ∀ {x y : ℝ}, 0 < y → ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Truncated.Hom.tr_comp_assoc : ∀ {n : ℕ} {a b c : SimplexCategory} (f : a ⟶ b) (g : b ⟶ c)
  (ha : autoParam (a.len ≤ n) SimplexCategory.Truncated.Hom.tr_comp._auto_1)
  (hb : autoParam (b.len ≤ n) SimplexCategory.Truncated.Hom.tr_comp._auto_3)
  (hc : autoParam (c.len ≤ n) SimplexCategory.Truncated.Hom.tr_comp._auto_5)
  {Z : CategoryTheory.ObjectProperty.FullSubcategory fun a => a.len ≤ n} (h : { obj := c, property := hc } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.Hom.tr (CategoryTheory.CategoryStruct.comp f g) ha hc)
      h =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.Hom.tr f ha hb)
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.Hom.tr g hb hc) h)
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instProductivenessRelation : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LE α] →
      [inst_2 : DecidableLE α] →
        [Std.PRange.LawfulUpwardEnumerable α] → Std.Iterators.ProductivenessRelation (Std.Rxc.Iterator α) Id
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.graph.eq_1 : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F),
  f.graph = Submodule.map (f.domain.subtype.prodMap LinearMap.id) f.toFun.graph
-- Mathlib.Order.Ideal
Order.Ideal.principal_le_iff : ∀ {P : Type u_1} [inst : Preorder P] {I : Order.Ideal P} {x : P}, Order.Ideal.principal x ≤ I ↔ x ∈ I
-- Mathlib.Algebra.Group.Subgroup.Finite
AddMonoidHom.decidableMemRange.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_3} [inst_1 : AddGroup N] (f : G →+ N) [inst_2 : Fintype G]
  [inst_3 : DecidableEq N] (x : N), f.decidableMemRange x = Fintype.decidableExistsFintype
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.WF.rank_eq : ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {n : ℕ} {s : Batteries.BinomialHeap.Imp.HeapNode α},
  Batteries.BinomialHeap.Imp.HeapNode.WF le a s n → s.rank = n
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k fallback : α}, k ∉ m₁ → (m₁ ∩ m₂).getKeyD k fallback = fallback
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
/-- Jacobi's one-variable theta function `∑' (n : ℤ), exp (π * I * n ^ 2 * τ)`.  -/
jacobiTheta : ℂ → ℂ
-- Mathlib.Algebra.Group.Commute.Units
Commute.units_zpow_left : ∀ {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ}, Commute (↑u) a → ∀ (m : ℤ), Commute (↑(u ^ m)) a
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.ctor.sizeOf_spec : ∀ (i : Lean.IR.CtorInfo) (ys : Array Lean.IR.Arg), sizeOf (Lean.IR.Expr.ctor i ys) = 1 + sizeOf i + sizeOf ys
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for monotonicity of addition on the left,
namely `b₁ < b₂ → a + b₁ < a + b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedAddMonoid`.  -/
AddLeftStrictMono : (M : Type u_1) → [Add M] → [LT M] → Prop
-- Mathlib.Algebra.BigOperators.Pi
AddMonoidHom.functions_ext'_iff : ∀ {I : Type u_7} [inst : DecidableEq I] {M : I → Type u_8} [inst_1 : (i : I) → AddCommMonoid (M i)] [Finite I]
  {N : Type u_9} [inst_3 : AddCommMonoid N] {g h : ((i : I) → M i) →+ N},
  g = h ↔ ∀ (i : I), g.comp (AddMonoidHom.single M i) = h.comp (AddMonoidHom.single M i)
-- Batteries.Tactic.OpenPrivate
/-- Get the module index given a module name.  -/
Lean.Environment.moduleIdxForModule? : Lean.Environment → Lean.Name → Option Lean.ModuleIdx
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
/-- If `3 ≤ Nat.card α`, then `alternatingGroup α` acts transitively on `Set.powersetCard α n`.

If `Nat.card α ≤ 2`, then `alternatingGroup α` is trivial, and
the result only holds in the trivial case where `powersetCard α n` is a subsingleton,
that is, when `n = 0` or `Nat.card α ≤ n`.  -/
Set.powersetCard.isPretransitive_alternatingGroup : ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
  3 ≤ Nat.card α → MulAction.IsPretransitive ↥(alternatingGroup α) ↑(Set.powersetCard α n)
-- Mathlib.Logic.Equiv.Multiset
Denumerable.isChain_raise : ∀ (l : List ℕ) (n : ℕ), List.IsChain (fun x1 x2 => x1 ≤ x2) (Denumerable.raise l n)
-- Init.Data.List.TakeDrop
List.dropWhile_append_of_pos : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α},
  (∀ a ∈ l₁, p a = true) → List.dropWhile p (l₁ ++ l₂) = List.dropWhile p l₂
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.substFunc.match_1.eq_2 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u_3}
  (motive : L.Term α → ({n : ℕ} → L.Functions n → L'.Term (Fin n)) → Sort u_6) (l : ℕ) (f : L.Functions l)
  (ts : Fin l → L.Term α) (tf : {n : ℕ} → L.Functions n → L'.Term (Fin n))
  (h_1 : (a : α) → (x : {n : ℕ} → L.Functions n → L'.Term (Fin n)) → motive (FirstOrder.Language.var a) x)
  (h_2 :
    (l : ℕ) →
      (f : L.Functions l) →
        (ts : Fin l → L.Term α) →
          (tf : {n : ℕ} → L.Functions n → L'.Term (Fin n)) → motive (FirstOrder.Language.func f ts) tf),
  (match FirstOrder.Language.func f ts, tf with
    | FirstOrder.Language.var a, x => h_1 a x
    | FirstOrder.Language.func f ts, tf => h_2 l f ts tf) =
    h_2 l f ts tf
-- Init.Data.Repr
List.repr' : {α : Type u_1} → [Repr α] → [ReprAtom α] → List α → ℕ → Std.Format
-- Std.Data.Internal.List.Associative
Std.Internal.List.keys_cons : ∀ {α : Type u} {β : α → Type v} {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.keys (⟨k, v⟩ :: l) = k :: Std.Internal.List.keys l
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_midpoint_right : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V]
  [inst_5 : Invertible 2] (p₁ p₂ : P), nndist (midpoint 𝕜 p₁ p₂) p₂ = ‖2‖₊⁻¹ * nndist p₁ p₂
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [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}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : DecidableEq ι] [inst_7 : Fintype ι],
  IsLieAbelian ↥(RootPairing.GeckConstruction.cartanSubalgebra b)
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.T_S_rel_smul : ∀ {m : ℤ} (A : FixedDetMatrix (Fin 2) ℤ m),
  ModularGroup.S •
      ModularGroup.S • ModularGroup.S • ModularGroup.T • ModularGroup.S • ModularGroup.T • ModularGroup.S • A =
    ModularGroup.T⁻¹ • A
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.ofRestrict_stalkMap_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {U : TopCat}
  (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U),
  CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (X.ofRestrict h) x)
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C]
  (x x_1 x_2 : CategoryTheory.Arrow C),
  CategoryTheory.MonoidalCategoryStruct.associator x x_1 x_2 =
    CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator x x_1 x_2
-- Mathlib.Algebra.Group.Action.Defs
vadd_zero_add : ∀ {M : Type u_9} {N : Type u_10} [inst : AddZeroClass N] [inst_1 : VAdd M N] [VAddAssocClass M N N] (x : M) (y : N),
  (x +ᵥ 0) + y = x +ᵥ y
-- Mathlib.Data.Rat.Star
Rat.addSubmonoid_closure_range_pow : ∀ {n : ℕ}, n ≠ 0 → Even n → AddSubmonoid.closure (Set.range fun x => x ^ n) = AddSubmonoid.nonneg ℚ
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.tilted_mul_apply_mgf' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {s : Set Ω},
  MeasurableSet s →
    (μ.tilted fun x => t * X x) s =
      ∫⁻ (a : Ω) in s, ENNReal.ofReal (Real.exp (t * X a) / ProbabilityTheory.mgf X μ t) ∂μ
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_mul : ∀ {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₁ x₂ : R) (y₁ y₂ : ↥M),
  IsLocalization.mk' S (x₁ * x₂) (y₁ * y₂) = IsLocalization.mk' S x₁ y₁ * IsLocalization.mk' S x₂ y₂
-- Init.Prelude
Nat.pred_le : ∀ (n : ℕ), n.pred ≤ n
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsIso.inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.MorphismProperty C) [P.RespectsIso]
  [Q.RespectsIso], (P ⊓ Q).RespectsIso
-- Mathlib.Logic.Equiv.Fin.Basic
/-- Promote a `Fin n` into a larger `Fin m`, as a subtype where the underlying
values are retained.

This is the `Equiv` version of `Fin.castLE`.  -/
Fin.castLEquiv : {n m : ℕ} → n ≤ m → Fin n ≃ { i // ↑i < n }
-- Init.System.IOError
IO.Error.mkNoFileOrDirectory : String → UInt32 → String → IO.Error
-- Mathlib.RingTheory.Finiteness.Finsupp
MonoidAlgebra.moduleFinite : ∀ {M : Type u_1} {R : Type u_2} {S : Type u_3} [Finite M] [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] [Module.Finite R S], Module.Finite R (MonoidAlgebra S M)
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.process.processAppWithInfo : Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Sym.ProofInstInfo → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.Topology.UniformSpace.Basic
IsOpen.relComp : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {s : SetRel α β} {t : SetRel β γ}, IsOpen s → IsOpen t → IsOpen (s.comp t)
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.Monic.isPrimitive : ∀ {R : Type u_1} [inst : CommSemiring R] {p : Polynomial R}, p.Monic → p.IsPrimitive
-- Mathlib.Data.Sym.Sym2
/-- Mapping an unordered pair to an unordered list produces a multiset of size `2`.  -/
Sym2.card_toMultiset : ∀ {α : Type u_4} (z : Sym2 α), z.toMultiset.card = 2
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.compl_compl : ∀ {α : Type u_1} [inst : LE α] (s : UpperSet α), s.compl.compl = s
-- Init.Data.List.Range
_private.Init.Data.List.Range.0.List.range'.match_1.splitter : (motive : ℕ → ℕ → ℕ → Sort u_1) →
  (x x_1 x_2 : ℕ) → ((x x_3 : ℕ) → motive x 0 x_3) → ((s n step : ℕ) → motive s n.succ step) → motive x x_1 x_2
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Filter.EventuallyEq.iteratedDerivWithin_eq_of_nhds_insert : ∀ {𝕜 : Type u_7} {F : Type u_8} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (n : ℕ) {f g : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  f =ᶠ[nhdsWithin x (insert x s)] g → iteratedDerivWithin n f s x = iteratedDerivWithin n g s x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_filter_eq_false_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool},
  m.WF →
    ((Std.DHashMap.Raw.filter f m).isEmpty = false ↔
      ∃ k, ∃ (h : k ∈ m), f (m.getKey k h) (Std.DHashMap.Raw.Const.get m k h) = true)
-- Mathlib.Algebra.Order.Star.Real
/-- Although the instance `RCLike.toStarOrderedRing` exists, it is locked behind the
`ComplexOrder` scope because currently the order on `ℂ` is not enabled globally. But we
want `StarOrderedRing ℝ` to be available globally, so we include this instance separately.
In addition, providing this instance here makes it available earlier in the import
hierarchy; otherwise in order to access it we would need to import
`Mathlib/Analysis/RCLike/Basic.lean`.  -/
Real.instStarOrderedRing : StarOrderedRing ℝ
-- Aesop.Tree.Data
Aesop.RappData.children : {Goal MVarCluster : Type} → Aesop.RappData Goal MVarCluster → Array (IO.Ref MVarCluster)
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rci.Internal.forIn'_eq_forIn'_iter : ∀ {α : Type u} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_3 : Std.Rxi.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ}
  {m : Type u → Type w} [inst_5 : Monad m] {r : Std.Rci α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' (Std.Rci.Internal.iter r) init fun a ha acc => f a ⋯ acc
-- Lean.Widget.TaggedText
/-- The output is tagged with `(tag, indent)` where `tag` is from the input `Format` and `indent`
is the indentation level at this point. The latter is used to print sub-trees accurately by passing
it again as the `indent` argument.  -/
Lean.Widget.TaggedText.prettyTagged : Std.Format → optParam ℕ 0 → optParam ℕ Std.Format.defWidth → Lean.Widget.TaggedText (ℕ × ℕ)
-- Mathlib.Analysis.Complex.Basic
Complex.restrictScalars_toSpanSingleton : ∀ (x : ℂ), ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.toSpanSingleton ℂ x) = x • 1
-- Mathlib.Algebra.Module.Presentation.Basic
/-- If `M` admits a presentation by generators and relations, then
linear maps from `M` can be (naturally) identified to the solutions of
certain linear equations.  -/
Module.Relations.Solution.IsPresentation.linearMapEquiv : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module A M] →
            {solution : relations.Solution M} →
              solution.IsPresentation →
                {N : Type v'} → [inst_3 : AddCommGroup N] → [inst_4 : Module A N] → (M →ₗ[A] N) ≃ relations.Solution N
-- Mathlib.Tactic.GCongr.Core
/-- The context used by `GCongrM`.  -/
Mathlib.Tactic.GCongr.Context : Type