mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.DefEqM.Context.mk.inj : ∀ {unify zetaDelta : Bool} {lctxInitialNextIndex : ℕ} {mvarsNew mvarsToCheckType : Array Lean.MVarId}
  {unify_1 zetaDelta_1 : Bool} {lctxInitialNextIndex_1 : ℕ} {mvarsNew_1 mvarsToCheckType_1 : Array Lean.MVarId},
  { unify := unify, zetaDelta := zetaDelta, lctxInitialNextIndex := lctxInitialNextIndex, mvarsNew := mvarsNew,
        mvarsToCheckType := mvarsToCheckType } =
      { unify := unify_1, zetaDelta := zetaDelta_1, lctxInitialNextIndex := lctxInitialNextIndex_1,
        mvarsNew := mvarsNew_1, mvarsToCheckType := mvarsToCheckType_1 } →
    unify = unify_1 ∧
      zetaDelta = zetaDelta_1 ∧
        lctxInitialNextIndex = lctxInitialNextIndex_1 ∧ mvarsNew = mvarsNew_1 ∧ mvarsToCheckType = mvarsToCheckType_1
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- Equal maps of arrows are left homotopic.  -/
CategoryTheory.Arrow.LeftHomotopy.ofEq : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} → {f g : u ⟶ v} → f = g → CategoryTheory.Arrow.LeftHomotopy f g
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.isAddHaarMeasure_hausdorffMeasure : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E],
  (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)).IsAddHaarMeasure
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.coe_rangeRestrict : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (g : G), ↑(f.rangeRestrict g) = f g
-- Init.Data.Array.Basic
/-- Returns the first non-`none` result of applying the monadic function `f` to each element of the
array, in order. Returns `none` if `f` returns `none` for all elements.

Example:
```lean example
#eval #[7, 6, 5, 8, 1, 2, 6].findSomeM? fun i => do
  if i < 5 then
    return some (i * 10)
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return none
```
```output
Almost! 6
Almost! 5
```
```output
some 10
```
 -/
Array.findSomeM? : {α : Type u} → {β : Type v} → {m : Type v → Type w} → [Monad m] → (α → m (Option β)) → Array α → m (Option β)
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_real_eq_id : RCLike.ofReal = id
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toSubmodule_toNonUnitalSubalgebra : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  (S : NonUnitalSubalgebra R A), S.toSubmodule.toNonUnitalSubalgebra ⋯ = S
-- Mathlib.MeasureTheory.Function.EssSup
essSup_count_eq_ciSup : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : ConditionallyCompleteLattice β] {f : α → β} [Nonempty α]
  [MeasurableSingletonClass α], BddAbove (Set.range f) → essSup f MeasureTheory.Measure.count = ⨆ a, f a
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.trace_adjMatrix : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : AddCommMonoid α] [inst_3 : One α], (SimpleGraph.adjMatrix α G).trace = 0
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.centralizer_univ : ∀ {R : Type u_1} [inst : NonUnitalRing R], NonUnitalSubring.centralizer Set.univ = NonUnitalSubring.center R
-- Mathlib.Data.Fintype.Order
Finite.ciSup_prod : ∀ {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [Finite ι] [Finite ι'] [inst : ConditionallyCompleteLattice α]
  (f : ι × ι' → α), ⨆ a, f a = ⨆ i, ⨆ i', f (i, i')
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_toFinset : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] [inst_1 : DecidableEq α] (l : List α) (f : α → β)
  (comm : (↑l.toFinset).Pairwise (Function.onFun Commute f)),
  l.Nodup → l.toFinset.noncommProd f comm = (List.map f l).prod
-- Init.Data.UInt.Lemmas
UInt64.ofNatTruncate_toNat : ∀ (n : UInt64), UInt64.ofNatClamp n.toNat = n
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_of_support_subset : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] (f : α →₀ M) {s : Finset α},
  f.support ⊆ s → ∀ (g : α → M → N), (∀ i ∈ s, g i 0 = 0) → f.sum g = ∑ x ∈ s, g x (f x)
-- Mathlib.Topology.Basic
IsClosed.and : ∀ {X : Type u} {p₁ p₂ : X → Prop} [inst : TopologicalSpace X],
  IsClosed {x | p₁ x} → IsClosed {x | p₂ x} → IsClosed {x | p₁ x ∧ p₂ x}
-- Mathlib.Data.PEquiv
PEquiv.refl_trans : ∀ {α : Type u} {β : Type v} (f : α ≃. β), (PEquiv.refl α).trans f = f
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go.match_4.congr_eq_6 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (a b : Lean.Grind.CommRing.Expr),
  x = a.mul b →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.natCast k => h_2 k
      | Lean.Grind.CommRing.Expr.intCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_6 a b
-- Mathlib.Topology.Category.LightProfinite.Basic
instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyOfObj : ∀ (X : FintypeCat), Finite ↑(LightProfinite.of X.obj).toTop
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.IterM.step_take.match_3.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((k : ℕ) → motive k.succ) → motive n
-- Mathlib.Algebra.Opposites
AddOpposite.instNontrivial : ∀ {α : Type u_1} [Nontrivial α], Nontrivial αᵃᵒᵖ
-- Mathlib.LinearAlgebra.Determinant
LinearEquiv.coe_inv_det : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : M ≃ₗ[R] M),
  ↑(LinearEquiv.det f)⁻¹ = LinearMap.det ↑f.symm
-- Mathlib.Topology.Coherent
Topology.IsCoherentWith.mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S T : Set (Set X)},
  Topology.IsCoherentWith S → S ⊆ T → Topology.IsCoherentWith T
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.equivRange_apply_coe : ∀ {E : Type u_5} {F : Type u_9} [inst : SeminormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {R : Type u_11}
  {S : Type u_12} [inst_2 : Semiring R] [inst_3 : Ring S] [inst_4 : Module S E] [inst_5 : Module R F] {σ₁₂ : R →+* S}
  {σ₂₁ : S →+* R} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] (f : F →ₛₗᵢ[σ₁₂] E) (a : F),
  ↑(f.equivRange a) = f a
-- Mathlib.FieldTheory.Normal.Closure
/-- All `F`-`AlgHom`s from `K` to `L` factor through the normal closure of `K/F` in `L/F`.  -/
normalClosure.algHomEquiv : (F : Type u_1) →
  (K : Type u_2) →
    (L : Type u_3) →
      [inst : Field F] →
        [inst_1 : Field K] →
          [inst_2 : Field L] →
            [inst_3 : Algebra F K] →
              [inst_4 : Algebra F L] → (K →ₐ[F] ↥(IntermediateField.normalClosure F K L)) ≃ (K →ₐ[F] L)
-- Mathlib.Data.Nat.Totient
/-- When `p` is prime, then the totient of `p ^ (n + 1)` is `p ^ n * (p - 1)`  -/
Nat.totient_prime_pow_succ : ∀ {p : ℕ}, Nat.Prime p → ∀ (n : ℕ), (p ^ (n + 1)).totient = p ^ n * (p - 1)
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasStrictFDerivAt_exp_smul_const_of_mem_ball' : ∀ (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [inst : NontriviallyNormedField 𝕂] [CharZero 𝕂]
  [inst_2 : NormedCommRing 𝕊] [inst_3 : NormedRing 𝔸] [inst_4 : NormedSpace 𝕂 𝕊] [inst_5 : NormedAlgebra 𝕂 𝔸]
  [inst_6 : Algebra 𝕊 𝔸] [inst_7 : ContinuousSMul 𝕊 𝔸] [inst_8 : IsScalarTower 𝕂 𝕊 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕊),
  t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius →
    HasStrictFDerivAt (fun u => NormedSpace.exp (u • x))
      ((ContinuousLinearMap.smulRight 1 x).smulRight (NormedSpace.exp (t • x))) t
-- Mathlib.GroupTheory.Torsion
/-- The torsion additive subgroup of an additive abelian group.  -/
AddCommGroup.torsion : (G : Type u_1) → [inst : AddCommGroup G] → AddSubgroup G
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap.0.WeierstrassCurve.Affine.Point.sym2x.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (P Q : W'.Point),
  P.sym2x Q = ![P.xRep 0 * Q.xRep 0, P.xRep 0 * Q.xRep 1 + P.xRep 1 * Q.xRep 0, P.xRep 1 * Q.xRep 1]
-- Mathlib.Topology.MetricSpace.Antilipschitz
/-- If `f : α → β` is `0`-antilipschitz, then `α` is a `subsingleton`.  -/
AntilipschitzWith.subsingleton : ∀ {α : Type u_4} {β : Type u_5} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  AntilipschitzWith 0 f → Subsingleton α
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterMapM.match_1.eq_1 : ∀ {β β' : Type u_1} {n : Type u_1 → Type u_2} {f : β → n (Option β')} [inst : MonadAttach n] (out : β)
  (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) (hf : MonadAttach.CanReturn (f out) none)
  (h_1 : (hf : MonadAttach.CanReturn (f out) none) → motive ⟨none, hf⟩)
  (h_2 : (out' : β') → (hf : MonadAttach.CanReturn (f out) (some out')) → motive ⟨some out', hf⟩),
  (match ⟨none, hf⟩ with
    | ⟨none, hf⟩ => h_1 hf
    | ⟨some out', hf⟩ => h_2 out' hf) =
    h_1 hf
-- Init.Data.BitVec.Lemmas
/-- The msb at index `w-1` is the least significant bit, and is true when the width is nonzero.  -/
BitVec.getMsbD_one : ∀ {w i : ℕ}, (1#w).getMsbD i = (decide (i = w - 1) && decide (0 < w))
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of the reverse direction of `Finset.nonempty_Ioc`. -/
Finset.Aesop.nonempty_Ioc_of_lt : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], a < b → (Finset.Ioc a b).Nonempty
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
iteratedDeriv_cexp_const_mul : ∀ (n : ℕ) (c : ℂ), (iteratedDeriv n fun s => Complex.exp (c * s)) = fun s => c ^ n * Complex.exp (c * s)
-- Init.Data.Array.Erase
Array.eraseP_filterMap : ∀ {α : Type u_1} {β : Type u_2} {p : β → Bool} {f : α → Option β} {xs : Array α},
  (Array.filterMap f xs).eraseP p =
    Array.filterMap f
      (xs.eraseP fun x =>
        match f x with
        | some y => p y
        | none => false)
-- Init.Data.Vector.MapIdx
Vector.mapIdx_append : ∀ {α : Type u_1} {n m : ℕ} {α_1 : Type u_2} {f : ℕ → α → α_1} {xs : Vector α n} {ys : Vector α m},
  Vector.mapIdx f (xs ++ ys) = Vector.mapIdx f xs ++ Vector.mapIdx (fun i => f (i + n)) ys
-- Lean.Parser.Command
Lean.Parser.Command.openOnly.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Homeomorph.unitBall_apply_coe : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (a : E),
  ↑(Homeomorph.unitBall a) = ↑OpenPartialHomeomorph.univUnitBall a
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.locallyQuasiFinite_iff_finite_preimage_singleton : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.LocallyOfFiniteType f]
  [AlgebraicGeometry.QuasiCompact f], AlgebraicGeometry.LocallyQuasiFinite f ↔ ∀ (x : ↥Y), (⇑f ⁻¹' {x}).Finite
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} [inst_1 : SizeOf C] (f : A₀.a ⟶ A₁.a)
  (h :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map f) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str f)
      CategoryTheory.Endofunctor.Algebra.Hom.h._autoParam),
  sizeOf { f := f, h := h } = 1 + sizeOf f + sizeOf h
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.toUnit_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {Z : CategoryTheory.Over X},
  CategoryTheory.Over.Hom.left (CategoryTheory.SemiCartesianMonoidalCategory.toUnit Z) = Z.hom
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart.instIsLocallyFiniteMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : TopologicalSpace α]
  [MeasureTheory.IsLocallyFiniteMeasure μ], MeasureTheory.IsLocallyFiniteMeasure (μ.singularPart ν)
-- Mathlib.Algebra.Quandle
/-- The inverse actions of the elements  -/
Rack.invAct : {α : Type u} → [self : Rack α] → α → α → α
-- Mathlib.Topology.Algebra.ConstMulAction
ProperlyDiscontinuousSMul.exists_nhds_image_smul_eq_self : ∀ (Γ : Type u_4) {T : Type u_5} [inst : TopologicalSpace T] [inst_1 : SMul Γ T] [ProperlyDiscontinuousSMul Γ T]
  [T2Space T] [LocallyCompactSpace T] [ContinuousConstSMul Γ T] (x : T),
  ∃ U ∈ nhds x, ∀ (γ : Γ), ((fun x => γ • x) '' U ∩ U).Nonempty → γ • x = x
-- Mathlib.Data.List.ReduceOption
List.reduceOption_singleton : ∀ {α : Type u_1} (x : Option α), [x].reduceOption = x.toList
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.smooth_algebraMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (algebraMap R S).Smooth ↔ Algebra.Smooth R S
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- A recursor for `WithLowerSet`. Use as `induction x`.  -/
Topology.WithLowerSet.rec : {α : Type u_1} →
  {motive : Topology.WithLowerSet α → Sort u_4} →
    ((a : α) → motive (Topology.WithLowerSet.toLowerSet a)) → (a : Topology.WithLowerSet α) → motive a
-- Mathlib.RingTheory.Noetherian.Basic
/-- A submodule contained in an FG submodule is FG over noetherian rings.  -/
Submodule.FG.of_le : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherianRing R]
  {S T : Submodule R M}, T.FG → S ≤ T → S.FG
-- Mathlib.Data.EReal.Basic
/-- **Alias** of the reverse direction of `EReal.coe_le_coe_iff`. -/
EReal.coe_le_coe : ∀ {x y : ℝ}, x ≤ y → ↑x ≤ ↑y
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, ∅.size = 0
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sumAddHom_single : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i),
  ((DFinsupp.sumAddHom φ) fun₀ | i => x) = (φ i) x
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.mapsTo_eball : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (r : ENNReal), Set.MapsTo f (Metric.eball x r) (Metric.eball (f x) r)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_neg : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Neg R] (a : QuaternionAlgebra R c₁ c₂ c₃), (-a).imI = -a.imI
-- Mathlib.Algebra.Homology.Refinements
HomologicalComplex.eq_liftCycles_homologyπ_up_to_refinements : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} (K : HomologicalComplex C c) {A : C} {i : ι} (γ : A ⟶ K.homology i) (j : ι) (hj : c.next i = j),
  ∃ A' π,
    ∃ (_ : CategoryTheory.Epi π),
      ∃ z,
        ∃ (hz : CategoryTheory.CategoryStruct.comp z (K.d i j) = 0),
          CategoryTheory.CategoryStruct.comp π γ =
            CategoryTheory.CategoryStruct.comp (K.liftCycles z j hj hz) (K.homologyπ i)
-- Mathlib.Data.EReal.Basic
EReal.toReal_image_Ioo_bot_zero : EReal.toReal '' Set.Ioo ⊥ 0 = Set.Iio 0
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.PInfty_f_idem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (n : ℕ),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (AlgebraicTopology.DoldKan.PInfty.f n) =
    AlgebraicTopology.DoldKan.PInfty.f n
-- Mathlib.Algebra.BrauerGroup.Defs
IsBrauerEquivalent.is_eqv : ∀ {K : Type u} [inst : Field K], Equivalence IsBrauerEquivalent
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_add_left' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocDiv hp (p + a) b = toIocDiv hp a b - 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.c_relation_of_char_two : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 2], W.c₄ ^ 3 = W.c₆ ^ 2
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The equivalence of categories `ModuleCat S ≌ ModuleCat R` induced by `e : R ≃+* S`.  -/
ModuleCat.restrictScalarsEquivalenceOfRingEquiv : {R : Type u_1} → {S : Type u_2} → [inst : Ring R] → [inst_1 : Ring S] → R ≃+* S → (ModuleCat S ≌ ModuleCat R)
-- Mathlib.Topology.Algebra.Field
affineHomeomorph_image_Ioo : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [inst_4 : IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a),
  ⇑(affineHomeomorph a b ⋯) '' Set.Ioo c d = Set.Ioo (a * c + b) (a * d + b)
-- Mathlib.RingTheory.DedekindDomain.LinearDisjoint
IntermediateField.LinearDisjoint.basisOfBasisRight.congr_simp : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  (H : A.LinearDisjoint ↥B) (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤) {ι : Type u_1} (b b_1 : Module.Basis ι F ↥B),
  b = b_1 → H.basisOfBasisRight H' b = H.basisOfBasisRight H' b_1
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftComm_hom_comp_assoc : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] {X Y : C} (f : X ⟶ Y) (i j : A) {Z : C}
  (h : (CategoryTheory.shiftFunctor C i).obj ((CategoryTheory.shiftFunctor C j).obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm X i j).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C i).map ((CategoryTheory.shiftFunctor C j).map f)) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C j).map ((CategoryTheory.shiftFunctor C i).map f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm Y i j).hom h)
-- Mathlib.Algebra.BigOperators.Expect
/-- `Finset.expect_equiv` is a specialization of `Finset.expect_bij` that automatically fills in
most arguments.  -/
Finset.expect_equiv : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι}
  {f : ι → M} {t : Finset κ} {g : κ → M} (e : ι ≃ κ),
  (∀ (i : ι), i ∈ s ↔ e i ∈ t) → (∀ i ∈ s, f i = g (e i)) → (s.expect fun i => f i) = t.expect fun i => g i
-- Mathlib.RingTheory.Valuation.Basic
/-- An equivalence of valuations `v.IsEquiv w` induces the following map from `ValueGroup₀ v` to
`ValueGroup₀ w`: given `x : ValueGroup₀ v` and nonzero `a b : R` such that `(v a) * x = (v b)`,
`valueGroup₀Fun x` is defined as `(w b) * (w a)⁻¹`.  -/
Valuation.IsEquiv.valueGroup₀Fun : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    {Γ'₀ : Type u_5} →
      [inst : LinearOrderedCommGroupWithZero Γ₀] →
        [inst_1 : LinearOrderedCommGroupWithZero Γ'₀] →
          [inst_2 : Ring R] →
            {v : Valuation R Γ₀} →
              {w : Valuation R Γ'₀} →
                v.IsEquiv w → (MonoidWithZeroHom.ofClass v).ValueGroup₀ → (MonoidWithZeroHom.ofClass w).ValueGroup₀
-- Mathlib.Algebra.Polynomial.RuleOfSigns
_private.Mathlib.Algebra.Polynomial.RuleOfSigns.0.Polynomial.exists_cons_of_leadingCoeff_pos : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {P : Polynomial R} (η : R),
  0 < P.leadingCoeff →
    P.nextCoeff ≠ 0 →
      ∃ c₀ cs,
        ((Polynomial.X - Polynomial.C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
          ((Polynomial.X - Polynomial.C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
-- Lean.Elab.Tactic.Induction
/-- Given the goal `altMVarId` for a given alternative that introduces `numFields` new variables,
return the number of explicit variables. Recall that when the `@` is not used, only the explicit variables can
be named by the user.  -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.getNumExplicitFields : Lean.MVarId → ℕ → Lean.MetaM ℕ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {p p_1 : A → Prop} (e_p : p = p_1) [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] {a : A} (ha : p a), cfcₙHom ha = cfcₙHom ⋯
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
Std.Iterators.Types.DropWhile.PlausibleStep.skip : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} {it : Std.IterM m β} {it' : Std.IterM m β},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it') →
    Std.Iterators.Types.DropWhile.PlausibleStep it
      (Std.IterStep.skip (Std.IterM.Intermediate.dropWhileWithPostcondition P it.internalState.dropping it'))
-- Mathlib.RepresentationTheory.Basic
_private.Mathlib.RepresentationTheory.Basic.0.Representation.«term_⊗_» : Lean.TrailingParserDescr
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.le_def : ∀ (α β : Type u), Cardinal.mk α ≤ Cardinal.mk β ↔ Nonempty (α ↪ β)
-- Qq.Delab
_private.Qq.Delab.0.Qq.Impl.unquote : Lean.Expr → Qq.Impl.UnquoteM (Lean.Expr × Lean.LocalContext)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_zero : ∀ {R : Type u} {M : Type v} [inst : Zero R] [inst_1 : Zero M], TrivSqZeroExt.snd 0 = 0
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.decodeDecimalLitAux : String → String.Pos.Raw → ℕ → Option ℕ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.EqResult.decide.inj : ∀ {b b_1 : Bool}, Nat.EqResult.decide✝ b = Nat.EqResult.decide✝ b_1 → b = b_1
-- Mathlib.RingTheory.Henselian
HenselianLocalRing.mk : ∀ {R : Type u_1} [inst : CommRing R] [toIsLocalRing : IsLocalRing R],
  (∀ (f : Polynomial R),
      f.Monic →
        ∀ (a₀ : R),
          Polynomial.eval a₀ f ∈ IsLocalRing.maximalIdeal R →
            IsUnit (Polynomial.eval a₀ (Polynomial.derivative f)) →
              ∃ a, f.IsRoot a ∧ a - a₀ ∈ IsLocalRing.maximalIdeal R) →
    HenselianLocalRing R
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
/-- **Alias** of `AlgebraicGeometry.Scheme.Hom.finitePresentation_appLE`.

---

**Alias** of `AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_appLE`. -/
AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_of_affine_subset : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.LocallyOfFinitePresentation f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FinitePresentation
-- Init.Data.BitVec.Lemmas
BitVec.lt_intMin_iff_msb_eq_false : ∀ {w : ℕ} {x : BitVec w}, 0 < w → (x < BitVec.intMin w ↔ x.msb = false)