mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- `Scheme.Modules.pushforward` and `modulesSpecToSheaf` commute  -/
AlgebraicGeometry.pushforwardCompModulesSpecToSheafIso : {R S : CommRingCat} →
  (φ : R ⟶ S) →
    (AlgebraicGeometry.Scheme.Modules.pushforward (AlgebraicGeometry.Spec.map φ)).comp
        AlgebraicGeometry.modulesSpecToSheaf ≅
      AlgebraicGeometry.modulesSpecToSheaf.comp
        ((TopCat.Sheaf.pushforward (ModuleCat ↑S) (AlgebraicGeometry.Spec.map φ).base).comp
          (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(AlgebraicGeometry.Spec R))
            (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))))
-- Mathlib.Algebra.Quaternion
/-- Space of quaternions over a type, denoted as `ℍ[R]`.
Implemented as a structure with four fields: `re`, `im_i`, `im_j`, and `im_k`.  -/
Quaternion.«termℍ[_]» : Lean.ParserDescr
-- Init.Grind.AC
Lean.Grind.AC.Seq.unionFuel.match_3.congr_eq_2 : ∀ (motive : ℕ → Sort u_1) (fuel : ℕ) (h_1 : Unit → motive 0) (h_2 : (fuel : ℕ) → motive fuel.succ) (fuel_1 : ℕ),
  fuel = fuel_1.succ →
    (match fuel with
      | 0 => h_1 ()
      | fuel.succ => h_2 fuel) ≍
      h_2 fuel_1
-- Mathlib.RingTheory.Frobenius
/-- Suppose `S` is Noetherian and `Q` is a prime of `S` containing all zero divisors.
If `S/R` is unramified at `Q`, then the Frobenius `φ : S →ₐ[R] S` over `Q` is unique.  -/
AlgHom.IsArithFrobAt.eq_of_isUnramifiedAt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ ψ : S →ₐ[R] S}
  {Q : Ideal S},
  φ.IsArithFrobAt Q →
    ψ.IsArithFrobAt Q →
      ∀ [inst_3 : Q.IsPrime],
        Q.primeCompl ≤ nonZeroDivisors S → ∀ [Algebra.IsUnramifiedAt R Q] [IsNoetherianRing S], φ = ψ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.forIn_eq_forIn_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ},
  forIn t init f = forIn t.toArray init f
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_cases : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (P : A → Prop) (a : A)
  (f : R → R),
  P 0 →
    (∀ (hf : ContinuousOn f (quasispectrum R a))
        (h0 : { toFun := (quasispectrum R a).domRestrict f, continuous_toFun := ⋯ } 0 = 0) (ha : p a),
        P ((cfcₙHom ha) { toFun := (quasispectrum R a).domRestrict f, continuous_toFun := ⋯, map_zero' := h0 })) →
      P (cfcₙ f a)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∩ t₂).get? k = none
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- **Alias** of `SimpleGraph.isBridge_iff_forall_walk_mem_edges`. -/
SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges : ∀ {V : Type u} {G : SimpleGraph V} {v w : V}, G.IsBridge s(v, w) ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.tendsto_eval_ae_ae : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {i : ι},
  Filter.Tendsto (Function.eval i) (MeasureTheory.ae (MeasureTheory.Measure.pi μ)) (MeasureTheory.ae (μ i))
-- Lean.Meta.WHNF
Lean.Expr.toCtorIfLit : Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_left_le_size_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.size ≤ (t₁ ∪ t₂).size
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_eq_some_getElem!_of_contains : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m.WF → ∀ {a : α}, m.contains a = true → m[a]? = some m[a]!
-- Mathlib.Algebra.Module.Torsion.Basic
AddSubgroup.torsionBy.nsmul_iff : ∀ {A : Type u_3} [inst : AddCommGroup A] {n : ℕ} {x : A}, x ∈ AddSubgroup.torsionBy A ↑n ↔ n • x = 0
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.isHomogeneous : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  (I : HomogeneousIdeal 𝒜), Ideal.IsHomogeneous 𝒜 I.toIdeal
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.pOpcycles_opcyclesToCycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι)
  [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j] {Z : C} (h : K.cycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) h) =
    CategoryTheory.CategoryStruct.comp (K.toCycles i j) h
-- Std.Http.Transport
/-- Server to client direction.
 -/
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.SharedState.serverToClient : Std.Http.Internal.Mock.SharedState✝ → Std.CloseableChannel ByteArray
-- Mathlib.Topology.Sets.Closeds
/-- See Note [custom simps projection].  -/
TopologicalSpace.IrreducibleCloseds.Simps.coe : {α : Type u_2} → [inst : TopologicalSpace α] → TopologicalSpace.IrreducibleCloseds α → Set α
-- Mathlib.Order.Lattice.Nat
Nat.instInfSet : InfSet ℕ
-- Mathlib.Order.Irreducible
/-- **Alias** of the reverse direction of `supIrred_ofDual`. -/
InfIrred.ofDual : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : αᵒᵈ}, InfIrred a → SupIrred (OrderDual.ofDual a)
-- Mathlib.Order.UpperLower.Closure
LowerSet.sdiff_singleton : ∀ {α : Type u_1} [inst : Preorder α] (s : LowerSet α) (a : α), s.sdiff {a} = s.erase a
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_mul : ∀ (a b : UInt32), (a * b).toUInt8 = a.toUInt8 * b.toUInt8
-- Lean.Widget.InteractiveGoal
/-- The shared parts of interactive term-mode and tactic-mode goals.  -/
Lean.Widget.InteractiveGoalCore : Type
-- Mathlib.Tactic.FieldSimp
/-- `field` is a `simp` set that clears denominators in (semi-)field (in)equalities.

The `field` simp set is a variant of the `field_simp` tactic. The latter operates recursively on
subexpressions, bringing every field-expression encountered to the form `n / d`, and then attempts
to clear the denominator. (For confluence reasons, the `field` simprocs also have a slightly
different normal form from `field_simp`'s.)

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging
fails. These denominators are made out of denominators appearing in the input expression,
by repeatedly taking products or divisors. The discharger can be non-universal, i.e. can be specific
to the field at hand (order properties, explicit `≠ 0` hypotheses, `CharZero` if that is known,
etc). See `field_simp_discharge` for full details of the discharger algorithm.

* `simp [field, t₁, ..., tₙ]` provides terms `t₁`, ..., `tₙ` to the discharger for
  nonzeroness/positivity proofs.

Examples:
```
example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
    (x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
  simp only [field]
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
```
 -/
fieldEq : Lean.Meta.Simp.Simproc
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- If the quotient by the center of a group is cyclic, then the group is commutative.  -/
isAddCommutative_of_isAddCyclic_quotient_center_self : ∀ (G : Type u_2) [inst : AddGroup G] [IsAddCyclic (G ⧸ AddSubgroup.center G)], IsAddCommutative G
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.univ : BigOperators.FinsetResult✝
-- Mathlib.RingTheory.PowerSeries.Basic
/-- The coercion from polynomials to power series
as an algebra homomorphism.
 -/
Polynomial.coeToPowerSeries.algHom : {R : Type u_1} →
  [inst : CommSemiring R] →
    (A : Type u_2) → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Polynomial R →ₐ[R] PowerSeries A
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The natural transformation `S.opcycles ⟶ S.X₃` for all short complexes `S`.  -/
CategoryTheory.ShortComplex.fromOpcyclesNatTrans : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasKernels C] →
        [inst_3 : CategoryTheory.Limits.HasCokernels C] →
          CategoryTheory.ShortComplex.opcyclesFunctor C ⟶ CategoryTheory.ShortComplex.π₃
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.sum_sq_inner_right : ∀ {ι : Type u_1} [inst : Fintype ι] {E : Type u_7} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace ℝ E]
  (b : OrthonormalBasis ι ℝ E) (x : E), ∑ i, inner ℝ (b i) x ^ 2 = ‖x‖ ^ 2
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Split.instInhabitedState.default : Lean.Meta.Grind.Split.State
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_congr_measure_of_add_right : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C C' : ℝ} {μ' : MeasureTheory.Measure α}
  (hT_add : MeasureTheory.DominatedFinMeasAdditive (μ + μ') T C') (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (f : α → E),
  MeasureTheory.Integrable f (μ + μ') → MeasureTheory.setToFun (μ + μ') T hT_add f = MeasureTheory.setToFun μ T hT f
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
isMIntegralCurveOn_comp_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {s : Set ℝ} {dt : ℝ},
  IsMIntegralCurveOn (γ ∘ fun x => x + dt) v {t | t + dt ∈ s} ↔ IsMIntegralCurveOn γ v s
-- Init.Prelude
/-- The byte position of the end of the string slice.  -/
Substring.Raw.stopPos : Substring.Raw → String.Pos.Raw
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.map_top : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂), Submodule.map f ⊤ = f.range
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_one_eqOn : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A],
  Set.EqOn (fun a => a ^ 1) id (Set.Ici 0)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α}, k ∈ t.insertManyIfNewUnit l ↔ k ∈ t ∨ l.contains k = true
-- Init.Internal.Order.Basic
_private.Init.Internal.Order.Basic.0.EST.bind.match_1.splitter : {ε σ α : Type} →
  (motive : EST.Out ε σ α → Sort u_1) →
    (x : EST.Out ε σ α) →
      ((a : α) → (s : Void σ) → motive (EST.Out.ok a s)) →
        ((e : ε) → (s : Void σ) → motive (EST.Out.error e s)) → motive x
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS₂_neg : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ), complEDS₂ b c d (-k) = complEDS₂ b c d k
-- Mathlib.Order.Shrink
equivShrink_symm_top : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Top α], (equivShrink α).symm ⊤ = ⊤
-- Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
/-- The subscheme structure on an irreducible component of a Noetherian scheme.  -/
AlgebraicGeometry.Scheme.irreducibleComponent : (X : AlgebraicGeometry.Scheme) →
  (Z : Set ↥X) → Z ∈ irreducibleComponents ↥X → [AlgebraicGeometry.IsNoetherian X] → AlgebraicGeometry.Scheme
-- Init.Data.Vector.Lemmas
Vector.forall_mem_append : ∀ {α : Type u_1} {n m : ℕ} {p : α → Prop} {xs : Vector α n} {ys : Vector α m},
  (∀ x ∈ xs ++ ys, p x) ↔ (∀ x ∈ xs, p x) ∧ ∀ x ∈ ys, p x
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- An auxiliary equivalence useful in the proofs about
`FormalMultilinearSeries.changeOriginSeries`: the set of triples `(k, l, s)`, where `s` is a
`Finset (Fin (k + l))` of cardinality `l` is equivalent to the set of pairs `(n, s)`, where `s` is a
`Finset (Fin n)`.

The forward map sends `(k, l, s)` to `(k + l, s)` and the inverse map sends `(n, s)` to
`(n - Finset.card s, Finset.card s, s)`. The actual definition is less readable because of problems
with non-definitional equalities.  -/
FormalMultilinearSeries.changeOriginIndexEquiv : (k : ℕ) × (l : ℕ) × { s // s.card = l } ≃ (n : ℕ) × Finset (Fin n)
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.degree_interpolate_erase_lt : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {i : ι} {v : ι → F}
  (r : ι → F), Set.InjOn v ↑s → i ∈ s → ((Lagrange.interpolate (s.erase i) v) r).degree < ↑(s.card - 1)
-- Mathlib.RingTheory.Localization.BaseChange
LocalizedModule.equivTensorProduct_symm_apply_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (x : M) (r : R) (s : ↥S),
  (LocalizedModule.equivTensorProduct S M).symm (Localization.mk r s ⊗ₜ[R] x) = r • LocalizedModule.mk x s
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
/-- Compose two isomorphisms in a monoidal category,
inserting unitors and associators between as necessary.  -/
CategoryTheory.monoidalIsoComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} → [CategoryTheory.MonoidalCoherence X Y] → (W ≅ X) → (Y ≅ Z) → (W ≅ Z)
-- Mathlib.Logic.Equiv.Basic
/-- A sigma of a sigma whose second base does not depend on the first is equivalent
to a sigma whose base is a product.  -/
Equiv.sigmaAssocProd : {α : Type u_9} → {β : Type u_10} → {γ : α → β → Type u_11} → (ab : α × β) × γ ab.1 ab.2 ≃ (a : α) × (b : β) × γ a b
-- Mathlib.Combinatorics.SimpleGraph.Cayley
/-- `mulCayley` is a left (order-)adjoint.  -/
SimpleGraph.mulCayley_gc : ∀ (M : Type u_1) [inst : Mul M],
  GaloisConnection (fun x => SimpleGraph.mulCayley x) fun x => {g | ∀ (a : M), a * g ≠ a → x.Adj (a * g) a}
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `L` are linearly disjoint, one of them is algebraic, then for any `B` and `L'`
isomorphic to `A` and `L` respectively, `B` and `L'` are also linearly disjoint.  -/
IntermediateField.LinearDisjoint.algEquiv_of_isAlgebraic : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    ∀ {E' : Type u_1} [inst_7 : Field E'] [inst_8 : Algebra F E'] (B : IntermediateField F E') (L' : Type u_2)
      [inst_9 : Field L'] [inst_10 : Algebra F L'] [inst_11 : Algebra L' E'] [inst_12 : IsScalarTower F L' E']
      (f1 : ↥A ≃ₐ[F] ↥B) (f2 : L ≃ₐ[F] L'), Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L → B.LinearDisjoint L'
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.AffineOpenCover.ofIsOpenCover_I₀ : ∀ {X : AlgebraicGeometry.Scheme} {ι : Type u_1} (U : ι → X.Opens) (hU : TopologicalSpace.IsOpenCover U)
  (hU' : ∀ (i : ι), AlgebraicGeometry.IsAffineOpen (U i)),
  (AlgebraicGeometry.Scheme.AffineOpenCover.ofIsOpenCover U hU hU').I₀ = ι
-- Mathlib.CategoryTheory.Subfunctor.Subobject
CategoryTheory.Subfunctor.equivalenceMonoOver_inverse_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w))
  {X Y : CategoryTheory.MonoOver F} (f : X ⟶ Y),
  (CategoryTheory.Subfunctor.equivalenceMonoOver F).inverse.map f = CategoryTheory.homOfLE ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.hasHomology_of_isIsoLeftRightHomologyComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : S.HasLeftHomology] [inst_3 : S.HasRightHomology]
  [h : CategoryTheory.IsIso S.leftRightHomologyComparison], S.HasHomology
-- Mathlib.Data.Subtype
/-- Defining a map into a subtype, this can be seen as a "coinduction principle" of `Subtype`  -/
Subtype.coind : {α : Sort u_4} → {β : Sort u_5} → (f : α → β) → {p : β → Prop} → (∀ (a : α), p (f a)) → α → Subtype p
-- Mathlib.Logic.Hydra
Relation.CutExpand.eq_1 : ∀ {α : Type u_1} (r : α → α → Prop) (s' s : Multiset α),
  Relation.CutExpand r s' s = ∃ t a, (∀ a' ∈ t, r a' a) ∧ s' + {a} = s + t
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inr_mul_inl : ∀ {R : Type u_1} {A : Type u_2} [inst : MulZeroClass R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : SMulZeroClass R A] (r : R) (a : A), ↑a * Unitization.inl r = ↑(r • a)
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_closure : ∀ {R : Type u_2} [inst : NonAssocRing R] (s : Set R), (Subring.closure s).op = Subring.closure (MulOpposite.unop ⁻¹' s)
-- Init.Data.Rat.Lemmas
Rat.divInt_neg' : ∀ (num den : ℤ), Rat.divInt num (-den) = Rat.divInt (-num) den
-- Mathlib.RingTheory.PrincipalIdealDomain
IsBezout.gcd_dvd_left : ∀ {R : Type u} [inst : CommRing R] (x y : R) [inst_1 : Submodule.IsPrincipal (Ideal.span {x, y})], IsBezout.gcd x y ∣ x
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  (f : α → C),
  CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure✝ f 0 = ⟨ULift.{v, w} α, f ∘ ULift.down⟩
-- Mathlib.Analysis.RCLike.Lemmas
convex_RCLike_iff_convex_real : ∀ {K : Type u_1} {E : Type u_2} [inst : RCLike K] [inst_1 : AddCommMonoid E] [inst_2 : Module K E] [inst_3 : Module ℝ E]
  [IsScalarTower ℝ K E] {s : Set E}, Convex K s ↔ Convex ℝ s
-- Lean.Meta.Tactic.AuxLemma
/-- Helper method for creating auxiliary lemmas in the environment.

It uses a cache that maps `type` to declaration name. The cache is not stored in `.olean` files.
It is useful to make sure the same auxiliary lemma is not created over and over again in the same
environment branch. For expensive auxiliary lemmas that should be deduplicated even across
different environment branches, consider using `realizeConst` instead.

This method is useful for tactics (e.g., `simp`) that may perform preprocessing steps to lemmas provided by
users. For example, `simp` preprocessor may convert a lemma into multiple ones.
 -/
Lean.Meta.mkAuxLemma : List Lean.Name →
  Lean.Expr →
    Lean.Expr →
      optParam (Option Lean.Name) none →
        optParam Bool true → optParam Bool false → optParam Bool false → optParam Bool false → Lean.MetaM Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.pushout.whiskerLeft_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {Q : C},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q f)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inl f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q g)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inr f g))
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
/-- If `M` is nondegenerate and `w ≠ 0`, then there is some `v` such that `v * M * w ≠ 0`.  -/
Matrix.Nondegenerate.exists_not_ortho_of_ne_zero' : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Fintype m]
  [inst_2 : Fintype n], M.Nondegenerate → ∀ {w : n → R}, w ≠ 0 → ∃ v, v ⬝ᵥ M.mulVec w ≠ 0
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- The trivial monoid algebra is isomorphic to the base ring.  -/
AddMonoidAlgebra.bialgEquivOfSubsingleton : {R : Type u_1} →
  (M : Type u_8) → [inst : CommSemiring R] → [inst_1 : AddMonoid M] → [Subsingleton M] → AddMonoidAlgebra R M ≃ₐc[R] R
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_filter_le_size : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool},
  (Std.HashSet.filter f m).size ≤ m.size
-- Mathlib.Algebra.Group.Pi.Lemmas
AddMonoidHom.coeFn.eq_1 : ∀ (α : Type u_5) (β : Type u_6) [inst : AddZeroClass α] [inst_1 : AddCommMonoid β],
  AddMonoidHom.coeFn α β = { toFun := fun g => ⇑g, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.RingTheory.Localization.Defs
Localization.mk_algebraMap : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {A : Type u_4} [inst_1 : CommSemiring A]
  [inst_2 : Algebra A R] (m : A), Localization.mk ((algebraMap A R) m) 1 = (algebraMap A (Localization M)) m
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
/-- A certain explicit list of locally constant maps. The theorem `factors_prod_eq_basis` shows that the
product of the elements in this list is the delta function `spanFinBasis C s x`.
 -/
Profinite.NobelingProof.factors : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      (s : Finset I) →
        ↑(Profinite.NobelingProof.π C fun x => x ∈ s) →
          List (LocallyConstant ↑(Profinite.NobelingProof.π C fun x => x ∈ s) ℤ)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_insert_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.getKey k ⋯ = k
-- Init.Grind.AC
Lean.Grind.AC.Seq.denote : {α : Sort u_1} → Lean.Grind.AC.Context α → Lean.Grind.AC.Seq → α
-- Mathlib.Order.BoundedOrder.Basic
subsingleton_iff_top_eq_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α], ⊤ = ⊥ ↔ Subsingleton α
-- Plausible.Testable
/-- Combine the test result for properties `p` and `q` to create a test for their conjunction.  -/
Plausible.TestResult.and : {p q : Prop} → Plausible.TestResult p → Plausible.TestResult q → Plausible.TestResult (p ∧ q)
-- Mathlib.LinearAlgebra.UnitaryGroup
/-- The transpose of a unitary matrix as a unitary matrix.  -/
Matrix.UnitaryGroup.transpose : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {α : Type v} →
        [inst_2 : CommRing α] → [inst_3 : StarRing α] → ↥(Matrix.unitaryGroup n α) → ↥(Matrix.unitaryGroup n α)
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The `E₂` cohomological spectral sequence indexed by `ℤ × ℤ` attached to
a spectral object indexed by `EInt`.  -/
CategoryTheory.Abelian.SpectralObject.E₂SpectralSequence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.Abelian.SpectralObject C EInt → CategoryTheory.E₂CohomologicalSpectralSequence C
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuous.lowerHemicontinuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  LowerHemicontinuous f → ∀ (s : Set α), LowerHemicontinuousOn f s
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.closedBall_sdiff_sphere : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.closedBall x ε \ Metric.sphere x ε = Metric.ball x ε