mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.beq_iff_ne_notANumber_and_eq : ∀ (a b : Float.Model.UnpackedFloat),
  a.beq b = true ↔
    a ≠ Float.Model.UnpackedFloat.notANumber ∧
      b ≠ Float.Model.UnpackedFloat.notANumber ∧
        (a = b ∨
          a = Float.Model.UnpackedFloat.zero Float.Model.UnpackedFloat.Sign.positive ∧
              b = Float.Model.UnpackedFloat.zero Float.Model.UnpackedFloat.Sign.negative ∨
            a = Float.Model.UnpackedFloat.zero Float.Model.UnpackedFloat.Sign.negative ∧
              b = Float.Model.UnpackedFloat.zero Float.Model.UnpackedFloat.Sign.positive)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.lipschitzWith_one_eval : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] (p : ENNReal) [inst_1 : Fact (1 ≤ p)]
  (i : α), LipschitzWith 1 fun x => ↑x i
-- Mathlib.Analysis.Meromorphic.Basic
/-- If two functions differ only on a discrete set, then one is meromorphic iff so is the other.
 -/
meromorphic_congr_codiscrete : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E}, f =ᶠ[Filter.codiscrete 𝕜] g → (Meromorphic f ↔ Meromorphic g)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.id_apply : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E] (x : E),
  LinearIsometry.id x = x
-- Mathlib.Topology.DerivedSet
derivedSet_union : ∀ {X : Type u_1} [inst : TopologicalSpace X] (A B : Set X), derivedSet (A ∪ B) = derivedSet A ∪ derivedSet B
-- Init.GetElem
Array.instGetElemNatLtSize : {α : Type u_1} → GetElem (Array α) ℕ α fun xs i => i < xs.size
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.toReal_klDiv : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
      (InformationTheory.klDiv μ ν).toReal = ∫ (a : α), MeasureTheory.llr μ ν a ∂μ + ν.real Set.univ - μ.real Set.univ
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The `M`-equivariant functions from an additive monoid `M` to itself are exactly
right additions by elements of `M`.  -/
AddActionHom.End.equivAddOpposite : {M : Type u_2} → [inst : AddMonoid M] → (M →ₑ[id] M) ≃+ Mᵃᵒᵖ
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_bijective : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (c : P) {R : ℝ}, R ≠ 0 → Function.Bijective (EuclideanGeometry.inversion c R)
-- ProofWidgets.Cancellable
ProofWidgets.CheckRequestResponse.done.injEq : ∀ (result result_1 : ProofWidgets.LazyEncodable Lean.Json),
  (ProofWidgets.CheckRequestResponse.done result = ProofWidgets.CheckRequestResponse.done result_1) =
    (result = result_1)
-- Mathlib.Topology.Convenient.Category
/-- The category of `X`-generated spaces is coreflective in the category of topological spaces.  -/
GeneratedByTopCat.instCoreflectiveTopCatToTopCat : {ι : Type t} →
  {X : ι → Type u} → [inst : (i : ι) → TopologicalSpace (X i)] → CategoryTheory.Coreflective GeneratedByTopCat.toTopCat
-- Mathlib.Algebra.Group.Irreducible.Lemmas
irreducible_isUnit_mul : ∀ {M : Type u_2} [inst : Monoid M] {x y : M}, IsUnit x → (Irreducible (x * y) ↔ Irreducible y)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.centerToMulOpposite_apply_coe : ∀ {R : Type u} [inst : NonAssocRing R] (r : ↥(Subsemigroup.center R)),
  ↑(Subring.centerToMulOpposite r) = MulOpposite.op ↑r
-- Mathlib.RingTheory.Polynomial.SeparableDegree
/-- The separable degree divides the degree.  -/
Polynomial.HasSeparableContraction.dvd_degree : ∀ {F : Type u_1} [inst : CommSemiring F] {q : ℕ} {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f),
  hf.degree ∣ f.natDegree
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
cauchySeq_iff_tendsto_dist_atTop_0 : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [Nonempty β] [inst_2 : SemilatticeSup β] {u : β → α},
  CauchySeq u ↔ Filter.Tendsto (fun n => dist (u n.1) (u n.2)) Filter.atTop (nhds 0)
-- Init.Data.Int.DivMod.Lemmas
Int.decidableDvd : DecidableRel fun x1 x2 => x1 ∣ x2
-- Mathlib.RingTheory.ClassGroup.Basic
mem_principal_ideals_iff : ∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ},
  I ∈ (toPrincipalIdeal R K).range ↔ ∃ x, FractionalIdeal.spanSingleton (nonZeroDivisors R) x = ↑I
-- ProofWidgets.Component.PenroseDiagram
/-- Abbreviation for backwards-compatibility.  -/
ProofWidgets.PenroseDiagramProps : Type
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.norm_natCast_zmodRepr_eq : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]), ‖↑x.zmodRepr‖ = 1 ∨ x.zmodRepr = 0
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.categoryStruct : {B : Type u_1} →
  {C : Type u_2} →
    [CategoryTheory.Bicategory C] →
      {F : B → C} → CategoryTheory.CategoryStruct.{u_4, u_1} (CategoryTheory.Bicategory.InducedBicategory C F)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ordered_keys_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  List.Pairwise (fun a b => cmp a.1 b.1 = Ordering.lt) t.toList
-- Mathlib.Tactic.FunProp.FunctionData
/-- If head function is a let-fvar unfold it and return resulting function.
Return `none` otherwise.  -/
Mathlib.Meta.FunProp.FunctionData.unfoldHeadFVar? : Mathlib.Meta.FunProp.FunctionData → Lean.MetaM (Option Lean.Expr)
-- Mathlib.GroupTheory.Finiteness
AddSubgroup.FG.biSup_finset : ∀ {G : Type u_3} [inst : AddGroup G] {ι : Type u_5} (s : Finset ι) (P : ι → AddSubgroup G),
  (∀ i ∈ s, (P i).FG) → (⨆ i ∈ s, P i).FG
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.not_has_remove : ∀ (assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment) (b : Bool),
  ¬Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b
        (Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeAssignment b assignment) =
      true
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.length.eq_1 : ∀ {α : Type u_1} (a : FreeMonoid α), a.length = (FreeMonoid.toList a).length
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.Cache.mk.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {sα : Q(CommSemiring «$α»)} {rα : Option Q(CommRing «$α»)}
  {dsα : Option Q(Semifield «$α»)} {czα : Option Q(CharZero «$α»)} {rα_1 : Option Q(CommRing «$α»)}
  {dsα_1 : Option Q(Semifield «$α»)} {czα_1 : Option Q(CharZero «$α»)},
  { rα := rα, dsα := dsα, czα := czα } = { rα := rα_1, dsα := dsα_1, czα := czα_1 } →
    rα = rα_1 ∧ dsα = dsα_1 ∧ czα = czα_1
-- Mathlib.Order.Max
IsBot.isMin : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsBot a → IsMin a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} {fallback : β k}, k ∉ m₂ → (m₁ \ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- Two partial maps from reduced schemes to separated schemes are equivalent if and only if
they are equal on the intersection of the domains.  -/
AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated : ∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] [AlgebraicGeometry.IsReduced X]
  [AlgebraicGeometry.IsSeparated (Y ↘ S)] {f g : X.PartialMap Y} [AlgebraicGeometry.Scheme.PartialMap.IsOver S f]
  [AlgebraicGeometry.Scheme.PartialMap.IsOver S g],
  f.equiv g ↔ (f.restrict (f.domain ⊓ g.domain) ⋯ ⋯).hom = (g.restrict (f.domain ⊓ g.domain) ⋯ ⋯).hom
-- Init.Data.SInt.Lemmas
Int8.ofInt_lt_iff_lt : ∀ {a b : ℤ},
  Int8.minValue.toInt ≤ a →
    a ≤ Int8.maxValue.toInt → Int8.minValue.toInt ≤ b → b ≤ Int8.maxValue.toInt → (Int8.ofInt a < Int8.ofInt b ↔ a < b)
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.fromLeftNeg_eq_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (a : ↥S.leftNeg) (b : M),
  ↑(S.fromLeftNeg a) = b ↔ ↑a + b = 0
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_functor_eq' : ∀ {X U : TopCat} (f : U ⟶ X) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (V : TopologicalSpace.Opens ↑U), (TopologicalSpace.Opens.map f).obj (hf.functor.obj V) = V
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sOppSide_lineMap_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, x ∈ s → y ∉ s → ∀ {t : R}, t < 0 → s.SOppSide ((AffineMap.lineMap x y) t) y
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider a differentiable map `v : M → E₁` to a vector bundle, over a base map `b : M → B`, and
linear maps `ϕ m : E₁ (b m) → E₂ (b m)` depending smoothly on `m`.
One can apply `ϕ m` to `v m`, and the resulting map is differentiable.

We give here a version of this statement on a set.  -/
MDifferentiableOn.clm_bundle_apply : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} [inst : NontriviallyNormedField 𝕜]
  {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8} [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_10}
  [inst_13 : NormedAddCommGroup EB] [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_15 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B] {EM : Type u_12}
  [inst_18 : NormedAddCommGroup EM] [inst_19 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_20 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_21 : TopologicalSpace M] [inst_22 : ChartedSpace HM M]
  [inst_23 : FiberBundle F₁ E₁] [inst_24 : VectorBundle 𝕜 F₁ E₁] [inst_25 : FiberBundle F₂ E₂]
  [inst_26 : VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : (x : M) → E₁ (b x)} {s : Set M}
  [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
  {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)}, MDiff[s] (T% ϕ) → MDiff[s] (T% v) → MDiff[s] fun m => ⟨b m, ⋯⟩
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.nhdsKer_eq_lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLowerSet α] (s : Set α),
  nhdsKer s = ↑(lowerClosure s)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.range_coe : Set.range UpperHalfPlane.coe = UpperHalfPlane.upperHalfPlaneSet
-- Lean.ToExpr
Lean.instToExprFVarId : Lean.ToExpr Lean.FVarId
-- Lean.Meta.InferType
Lean.Meta.throwIncorrectNumberOfLevels : {α : Type} → Lean.Name → List Lean.Level → Lean.MetaM α
-- Mathlib.Topology.Connected.LocallyConnected
locallyConnectedSpace_iff_connected_subsets : ∀ {α : Type u} [inst : TopologicalSpace α],
  LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ nhds x, ∃ V ∈ nhds x, IsPreconnected V ∧ V ⊆ U
-- Std.Do.PostCond
/-- A postcondition for the given predicate shape, with one `Assertion` for the terminating case and
one `Assertion` for each `.except` layer in the predicate shape.
```
variable (α σ ε : Type)
example : PostCond α (.arg σ .pure) = ((α → σ → ULift Prop) × PUnit) := rfl
example : PostCond α (.except ε .pure) = ((α → ULift Prop) × (ε → ULift Prop) × PUnit) := rfl
example : PostCond α (.arg σ (.except ε .pure)) = ((α → σ → ULift Prop) × (ε → ULift Prop) × PUnit) := rfl
example : PostCond α (.except ε (.arg σ .pure)) = ((α → σ → ULift Prop) × (ε → σ → ULift Prop) × PUnit) := rfl
```
 -/
Std.Do.PostCond : Type u → Std.Do.PostShape → Type u
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
/-- Do not use this field directly: use the more general
`guitartExact_of_isRightDerivabilityStructure` instead,
see also the lemma `isRightDerivabilityStructure_iff`.  -/
CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.guitartExact' : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C₁}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
  [self : Φ.IsRightDerivabilityStructure],
  CategoryTheory.TwoSquare.GuitartExact
    (CategoryTheory.CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.main : {k : Lean.SyntaxNodeKinds} →
  Lean.Elab.Term.MatchAltView k → Lean.Elab.Term.CollectPatternVars.M (Lean.Elab.Term.MatchAltView k)
-- Mathlib.GroupTheory.Coset.Basic
/-- A (non-canonical) bijection between a group `α` and the product `(α/s) × s`  -/
Subgroup.groupEquivQuotientProdSubgroup : {α : Type u_1} → [inst : Group α] → {s : Subgroup α} → α ≃ (α ⧸ s) × ↥s
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Denumerable.eqv.eq_1 : ∀ (α : Type u_3) [inst : Denumerable α],
  Denumerable.eqv α = { toFun := Encodable.encode, invFun := Denumerable.ofNat α, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Array.Zip
_private.Init.Data.Array.Zip.0.List.getElem?_zipWith.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          ((a : α) → (b : β) → motive (some a) (some b)) →
            ((x : Option α) →
                (x_2 : Option β) → (∀ (a : α) (b : β), x = some a → x_2 = some b → False) → motive x x_2) →
              motive x x_1
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.mk_eq_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {w₁ w₂ : FreeMonoid (M ⊕ N)},
  Monoid.Coprod.mk w₁ = Monoid.Coprod.mk w₂ ↔ (Monoid.coprodCon M N) w₁ w₂
-- Mathlib.Data.Seq.Computation
Computation.get_eq_of_promises : ∀ {α : Type u} (s : Computation α) [h : s.Terminates] {a : α}, s.Promises a → s.get = a
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Context.mk.sizeOf_spec : ∀ (letFVars : List Lean.FVarId), sizeOf { letFVars := letFVars } = 1 + sizeOf letFVars
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapAlgHom_single : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddMonoid M] (f : A →ₐ[R] B) (m : M)
  (a : A), (AddMonoidAlgebra.mapAlgHom M f) (AddMonoidAlgebra.single m a) = AddMonoidAlgebra.single m (f a)
-- Init.Data.Int.Gcd
Int.gcd_mul_left_left : ∀ (a b : ℤ), (a * b).gcd b = b.natAbs
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanImportClosureParams.mk.injEq : ∀ (importClosure importClosure_1 : Array Lean.Lsp.DocumentUri),
  ({ importClosure := importClosure } = { importClosure := importClosure_1 }) = (importClosure = importClosure_1)
-- Mathlib.Data.Int.Star
AddSubmonoid.nonneg.congr_simp : ∀ (M : Type u_1) [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : AddLeftMono M],
  AddSubmonoid.nonneg M = AddSubmonoid.nonneg M
-- Mathlib.Algebra.GCDMonoid.Basic
normUnit_mul_normUnit : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] (a : α), normUnit (a * ↑(normUnit a)) = 1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.minKeyD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {fallback : α},
  t₁.Equiv t₂ → t₁.minKeyD fallback = t₂.minKeyD fallback
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.bayesRisk_of_isEmpty : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [IsEmpty 𝓧], ProbabilityTheory.bayesRisk ℓ P π = 0
-- Std.Data.Iterators.Consumers.Set
/-- Traverses the given iterator and stores the emitted values in a {name}`ExtHashSet`.

If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α Id`,
the variant {lean}`it.ensureTermination.toExtHashSet` always terminates after finitely many steps.
 -/
Std.Iter.toExtHashSet : {α β : Type w} →
  [inst : BEq β] →
    [inst_1 : Hashable β] →
      [EquivBEq β] →
        [LawfulHashable β] → [inst_4 : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → Std.Iter β → Std.ExtHashSet β
-- Init.Tactics
/-- `with_unfolding_all tacs` executes `tacs` using the `.all` transparency setting.
In this setting all definitions that are not opaque are unfolded.
 -/
Lean.Parser.Tactic.withUnfoldingAll : Lean.ParserDescr
-- Mathlib.Algebra.GroupWithZero.Divisibility
eq_of_forall_dvd' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {a b : α} [Subsingleton αˣ],
  (∀ (c : α), c ∣ a ↔ c ∣ b) → a = b
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.arrayLit.injEq : ∀ (type : Lean.Expr) (xs : List Lean.Meta.Match.Pattern) (type_1 : Lean.Expr) (xs_1 : List Lean.Meta.Match.Pattern),
  (Lean.Meta.Match.Pattern.arrayLit type xs = Lean.Meta.Match.Pattern.arrayLit type_1 xs_1) =
    (type = type_1 ∧ xs = xs_1)
-- Init.Data.SInt.Lemmas
ISize.toInt32_sub : ∀ (a b : ISize), (a - b).toInt32 = a.toInt32 - b.toInt32
-- Mathlib.Topology.Partial
ptendsto'_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : Y →. X} {l : Filter Y} {x : X},
  Filter.PTendsto' f l (nhds x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f.preimage s ∈ l
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instMul : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [Mul M] → Mul (l.Germ M)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.inverse.eq_1 : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x : M₀), Ring.inverse x = if h : IsUnit x then ↑h.unit⁻¹ else 0
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.findEndSectionCompletionCandidates.mkCandidate : Array String → ℕ → String
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap.congr_simp : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X Y : C}
  (f f_1 : X ⟶ Y),
  f = f_1 →
    CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ f =
      CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ f_1
-- Std.Internal.Do.Order.PreservesSup
/-- The frame closure lies below the base transformer, witnessed at a unit resource `e` with
`op e = id`.  -/
Lean.Order.PreservesSup.frameClosure_le : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] {R : Type v} {β : Type w} (op : R → α → α)
  [∀ (r : R), Lean.Order.PreservesSup (op r)] (e : R),
  (∀ (a : α), op e a = a) →
    ∀ (k : (β → α) → α) (Q : β → α), Lean.Order.PartialOrder.rel (Lean.Order.PreservesSup.frameClosure op k Q) (k Q)
-- Mathlib.Order.Interval.Set.Basic
Set.right_notMem_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ∉ Set.Ioo b a
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.OverArrows.map₁_val : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A}
  {μ : G ⟶ A} {X : C} (s : CategoryTheory.yoneda.obj X ⟶ A) (u : CategoryTheory.OverPresheafAux.OverArrows η s)
  (ε : F ⟶ G) (hε : CategoryTheory.CategoryStruct.comp ε μ = η),
  (u.map₁ ε hε).val = (CategoryTheory.ConcreteCategory.hom (ε.app (Opposite.op X))) u.val
-- Mathlib.Analysis.Asymptotics.Theta
/-- **Alias** of the reverse direction of `Asymptotics.isTheta_const_mul_left`. -/
Asymptotics.IsTheta.const_mul_left : ∀ {α : Type u_1} {F : Type u_4} {𝕜 : Type u_14} [inst : Norm F] [inst_1 : NormedField 𝕜] {g : α → F} {l : Filter α}
  {c : 𝕜} {f : α → 𝕜}, c ≠ 0 → f =Θ[l] g → (fun x => c * f x) =Θ[l] g
-- Mathlib.Algebra.Algebra.Equiv
/-- Reinterpret a `RingEquiv` as a `ℤ`-algebra isomorphism.  -/
RingEquiv.toIntAlgEquiv : {R : Type u_1} → {S : Type u_2} → [inst : Ring R] → [inst_1 : Ring S] → R ≃+* S → R ≃ₐ[ℤ] S
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- Version of `Finsupp.sum_apply'` that applies in large generality to linear combinations
of functions in any `FunLike` type on which addition is defined pointwise.

At the time of writing Mathlib does not have a typeclass to express the condition
that addition on a `FunLike` type is pointwise; hence this is asserted via explicit hypotheses.  -/
Finsupp.sum_apply'' : ∀ {ι : Type u_2} {γ : Type u_3} {B : Type u_5} [inst : AddCommMonoid B] {A : Type u_16} {F : Type u_17}
  [inst_1 : AddZeroClass A] [inst_2 : AddCommMonoid F] [inst_3 : FunLike F γ B] (g : ι →₀ A) (k : ι → A → F) (x : γ),
  0 x = 0 → (∀ (f g : F), (f + g) x = f x + g x) → (g.sum k) x = g.sum fun i a => (k i a) x
-- Mathlib.Algebra.RingQuot
RingQuot.liftAlgHom_mkAlgHom_apply : ∀ (S : Type uS) [inst : CommSemiring S] {A : Type uA} [inst_1 : Semiring A] [inst_2 : Algebra S A] {B : Type u₄}
  [inst_3 : Semiring B] [inst_4 : Algebra S B] (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ ⦃x y : A⦄, s x y → f x = f y)
  (x : A), ((RingQuot.liftAlgHom S) ⟨f, w⟩) ((RingQuot.mkAlgHom S s) x) = f x
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.exp_log : ∀ {M : Type u_4} [inst : AddMonoid M] {x : WithZero (Multiplicative M)}, x ≠ 0 → WithZero.exp x.log = x
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
/-- **Zariski's main theorem**

Recall that any qcqs morphism `f : X ⟶ Y` factors through the relative normalization via
`f.toNormalization : X ⟶ f.normalization` (a dominant morphism) and
`f.fromNormalization : f.normalization ⟶ Y` (an integral morphism).

Let `f : X ⟶ Y` be separated and of finite type.

then there exists `U : f.normalization.Opens`, such that
1. `f.toNormalization ∣_ U` is an isomorphism
2. `f.toNormalization ⁻¹ᵁ U` is the quasi-finite locus of `f`
 -/
AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFiniteType f]
  [inst : AlgebraicGeometry.IsSeparated f] [inst_1 : AlgebraicGeometry.QuasiCompact f],
  ∃ U,
    CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.toNormalization f ∣_ U) ∧
      ((TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.toNormalization f).base).obj U).carrier =
        {x | AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x}
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x_3 : Std.DTreeMap.Internal.Impl.leaf.Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isGE = true),
  Std.DTreeMap.Internal.Impl.getEntryGE k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim