mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.reflexivePair.match_3.eq_6 : ∀ (motive : (X Y : CategoryTheory.Limits.WalkingReflexivePair) → (X ⟶ Y) → Sort u_1)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingReflexivePair) → motive x x (CategoryTheory.Limits.WalkingReflexivePair.Hom.id x))
  (h_2 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero
        CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
  (h_3 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero
        CategoryTheory.Limits.WalkingReflexivePair.Hom.right)
  (h_4 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)
  (h_5 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion)
  (h_6 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion),
  (match CategoryTheory.Limits.WalkingReflexivePair.one, CategoryTheory.Limits.WalkingReflexivePair.one,
      CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion with
    | x, .(x), CategoryTheory.Limits.WalkingReflexivePair.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.zero),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.left => h_2 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.zero),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.right => h_3 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.zero), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion => h_4 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion => h_5 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion => h_6 ()) =
    h_6 ()
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.repr.match_1.eq_2 : ∀ (motive : ONote → Sort u_1) (e : ONote) (n : ℕ+) (a : ONote) (h_1 : Unit → motive ONote.zero)
  (h_2 : (e : ONote) → (n : ℕ+) → (a : ONote) → motive (e.oadd n a)),
  (match e.oadd n a with
    | ONote.zero => h_1 ()
    | e.oadd n a => h_2 e n a) =
    h_2 e n a
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
/-- A distributive action of a monoid on a finite cyclic group of order `n` factors through an
action on `ZMod n`.  -/
MulDistribMulAction.toMonoidHomZModOfIsCyclic : (G : Type u_2) →
  [inst : Group G] →
    (M : Type u_4) →
      [inst_1 : Monoid M] → [IsCyclic G] → [MulDistribMulAction M G] → {n : ℕ} → Nat.card G = n → M →* ZMod n
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
/-- Markov's inequality for the counting measure with hypothesis using `tsum` in `ℝ≥0∞`.  -/
ENNReal.count_const_le_le_of_tsum_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {a : α → ENNReal},
  Measurable a →
    ∀ {c : ENNReal},
      ∑' (i : α), a i ≤ c → ∀ {ε : ENNReal}, ε ≠ 0 → ε ≠ ⊤ → MeasureTheory.Measure.count {i | ε ≤ a i} ≤ c / ε
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.HasOfPrecompProperty.of_precomp : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W W' : CategoryTheory.MorphismProperty C}
  [self : W.HasOfPrecompProperty W'] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  W' f → W (CategoryTheory.CategoryStruct.comp f g) → W g
-- Std.Data.DHashMap.Basic
Std.DHashMap.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α]
  [inst_3 : (a : α) → SizeOf (β a)] (inner : Std.DHashMap.Raw α β) (wf : inner.WF),
  sizeOf { inner := inner, wf := wf } = 1 + sizeOf inner + sizeOf wf
-- Mathlib.Analysis.Complex.Basic
/-- Continuous linear map version of the imaginary part function, from `ℂ` to `ℝ`.  -/
Complex.imCLM : ℂ →L[ℝ] ℝ
-- Mathlib.Combinatorics.SimpleGraph.Girth
/-- **Alias** of the reverse direction of `SimpleGraph.egirth_eq_top`. -/
SimpleGraph.IsAcyclic.egirth_eq_top : ∀ {α : Type u_1} {G : SimpleGraph α}, G.IsAcyclic → G.egirth = ⊤
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.mulSingle_mono : ∀ {I : Type u} {f : I → Type v} (i : I) [inst : DecidableEq I] [inst_1 : (i : I) → Preorder (f i)]
  [inst_2 : (i : I) → One (f i)], Monotone (Pi.mulSingle i)
-- Init.Prelude
/-- The notation typeclass for heterogeneous append.
This enables the notation `a ++ b : γ` where `a : α`, `b : β`.
 -/
HAppend : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Init.Data.List.MinMaxOn
List.maxOn_eq_minOn : ∀ {β : Type u_1} {α : Type u_2} {le : LE β} {dle : DecidableLE β} {xs : List α} {f : α → β} {h : xs ≠ []},
  List.maxOn f xs h = List.minOn f xs h
-- Init.Data.UInt.Lemmas
UInt16.toFin_toUInt64 : ∀ (n : UInt16), n.toUInt64.toFin = Fin.castLE UInt16.toFin_toUInt64._proof_1 n.toFin
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- The set in `Set (Arrow C)` which corresponds to `P : MorphismProperty C`.  -/
CategoryTheory.MorphismProperty.toSet : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Set (CategoryTheory.Arrow C)
-- Mathlib.Analysis.RCLike.Basic
Real.instRCLike : RCLike ℝ
-- Lean.Elab.PreDefinition.WF.GuessLex
_private.Lean.Elab.PreDefinition.WF.GuessLex.0.Lean.Elab.WF.GuessLex.generateCombinations?.goUniform : Array ℕ → ℕ → OptionT (StateM (Array (Array ℕ))) Unit
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.stableUnderSpecialization_image_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S)
  (Z : Set (PrimeSpectrum S)),
  IsClosed Z → (StableUnderSpecialization (PrimeSpectrum.comap f '' Z) ↔ IsClosed (PrimeSpectrum.comap f '' Z))
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.normUnit_X : ∀ {k : Type u_2} [inst : Field k], normUnit PowerSeries.X = 1
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.l_sSup_u_image : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisInsertion l u) (s : Set β), l (sSup (u '' s)) = sSup s
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.LocallyRingedSpace.instHasCoequalizer : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f g : X ⟶ Y), CategoryTheory.Limits.HasCoequalizer f g
-- Mathlib.Data.Complex.Basic
Complex.ofReal_add : ∀ (r s : ℝ), ↑(r + s) = ↑r + ↑s
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.summable_linear_sub_mul_linear_add : ∀ (z : ℂ) (c₁ c₂ : ℤ), Summable fun n => ((↑c₁ * z - ↑n) * (↑c₂ * z + ↑n))⁻¹
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.instTrans : {α : Type u} → Trans Std.HashSet.Raw.Equiv Std.HashSet.Raw.Equiv Std.HashSet.Raw.Equiv
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquash.inner : {α : Type v} → [small : Std.Internal.Small α] → Std.Internal.USquash α → Std.Internal.ComputableSmall.Target α
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RooSliceData : (α : Type u) → Type v → [Ord α] → Type (max u v)
-- Mathlib.Algebra.Group.Equiv.Defs
AddMonoid.End.equiv_apply : ∀ {M : Type u_9} [inst : AddZero M] (f : AddMonoid.End M) (x : M), ((AddMonoid.End.equiv M) f) x = f x
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.toAdditive.eq_1 : ∀ (R : Type u_3) (M : Type u_6) [inst : Semiring R] [inst_1 : Mul M],
  MonoidAlgebra.toAdditive R M =
    { toFun := fun x => AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff),
      invFun := fun x => MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.toMul) x.coeff), left_inv := ⋯,
      right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialTermInfo.mk.inj : ∀ {toElabInfo : Lean.Elab.ElabInfo} {lctx : Lean.LocalContext} {expectedType? : Option Lean.Expr}
  {toElabInfo_1 : Lean.Elab.ElabInfo} {lctx_1 : Lean.LocalContext} {expectedType?_1 : Option Lean.Expr},
  { toElabInfo := toElabInfo, lctx := lctx, expectedType? := expectedType? } =
      { toElabInfo := toElabInfo_1, lctx := lctx_1, expectedType? := expectedType?_1 } →
    toElabInfo = toElabInfo_1 ∧ lctx = lctx_1 ∧ expectedType? = expectedType?_1
-- Mathlib.Analysis.Normed.Group.Hom
/-- **Alias** of `NormedAddGroupHom.mkNormedAddGroupHom_norm_le'`.

---

If a bounded group homomorphism map is constructed from a group homomorphism
via the constructor `AddMonoidHom.mkNormedAddGroupHom`, then its norm is bounded by the bound
given to the constructor or zero if this bound is negative.  -/
AddMonoidHom.mkNormedAddGroupHom_norm_le' : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] (f : V₁ →+ V₂)
  {C : ℝ} (h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖), ‖f.mkNormedAddGroupHom C h‖ ≤ max C 0
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.ComplexEmbedding.conjugate.eq_1 : ∀ {K : Type u_1} [inst : Field K] (φ : K →+* ℂ), NumberField.ComplexEmbedding.conjugate φ = star φ
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.eq_1 : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A),
  spectrum R a = (resolventSet R a)ᶜ
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.isNontrivial_iff_isNontrivial : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommMonoidWithZero Γ₀]
  (v : Valuation R Γ₀) [v.Compatible], ValuativeRel.IsNontrivial R ↔ v.IsNontrivial
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.bi_min_div_two_pos : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), 0 < b (AkraBazziRecurrence.min_bi b) / 2
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.cons₁.inj : ∀ {a : Turing.ToPartrec.Code} {a_1 : Turing.PartrecToTM2.Cont'} {a_2 : Turing.ToPartrec.Code}
  {a_3 : Turing.PartrecToTM2.Cont'},
  Turing.PartrecToTM2.Cont'.cons₁ a a_1 = Turing.PartrecToTM2.Cont'.cons₁ a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.RingTheory.Etale.Basic
/-- Being étale is transported via algebra isomorphisms.  -/
Algebra.Etale.of_equiv : ∀ {R : Type u} {A : Type v} {B : Type u_1} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.Etale R A] (e : A ≃ₐ[R] B), Algebra.Etale R B
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- Let `adj : F ⊣ G` be an adjunction, with `G : D ⥤ C` reflective.
Assume that `D` has finite limits and `F` commutes with them.
If `C` has exact colimits of shape `J`, then `D` also has exact colimits of shape `J`.  -/
CategoryTheory.Adjunction.hasExactColimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u''} [inst_1 : CategoryTheory.Category.{v'', u''} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [G.Full] [G.Faithful] (J : Type u')
  [inst_4 : CategoryTheory.Category.{v', u'} J] [inst_5 : CategoryTheory.Limits.HasColimitsOfShape J C]
  [inst_6 : CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.HasExactColimitsOfShape J C]
  [CategoryTheory.Limits.HasFiniteLimits D] [CategoryTheory.Limits.PreservesFiniteLimits F],
  CategoryTheory.HasExactColimitsOfShape J D
-- Init.Data.UInt.Bitwise
UInt32.toBitVec_or : ∀ (a b : UInt32), (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianPDF.eq_1 : ∀ (μ : ℝ) (v : NNReal) (x : ℝ),
  ProbabilityTheory.gaussianPDF μ v x = ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal μ v x)
-- Init.Data.SInt.Lemmas
Int16.neg_ofInt : ∀ {n : ℤ}, -Int16.ofInt n = Int16.ofInt (-n)
-- Aesop.Tree.Data
Aesop.NodeState.unknown.sizeOf_spec : sizeOf Aesop.NodeState.unknown = 1
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.beq.eq_1 : Lean.Name.anonymous.beq Lean.Name.anonymous = true
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.muFun'.congr_simp : ∀ (𝕜 : Type u_2) {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] {inst_4 : DecidableEq α} [inst_5 : DecidableEq α] (b b_1 : α),
  b = b_1 → ∀ (a a_1 : α), a = a_1 → IncidenceAlgebra.muFun'✝ 𝕜 b a = IncidenceAlgebra.muFun'✝ 𝕜 b_1 a_1
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ihom_obj_V : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A : Rep.{w, u, v} k G) (B : Rep.{u_1, u, v} k G),
  ↑(A.ihom.obj B) = (↑A →ₗ[k] ↑B)
-- Std.Data.ExtTreeMap.Basic
/-- If there is no mapping for the given key, inserts the given mapping into the map. Otherwise,
returns the map unaltered.
 -/
Std.ExtTreeMap.insertIfNew : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → β → Std.ExtTreeMap α β cmp
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.instAddZeroClass.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoid.Coprod.instAddZeroClass =
    { zero := AddMonoid.Coprod.instAddZeroClass._aux_1, add := AddMonoid.Coprod.instAddZeroClass._aux_3, zero_add := ⋯,
      add_zero := ⋯ }
-- Mathlib.Analysis.Normed.Module.Basic
/-- Any normed characteristic-zero division ring that is a normed algebra over the reals is also a
normed algebra over the rationals.

Phrased another way, if `𝕜` is a normed algebra over the reals, then `AlgebraRat` respects that
norm.  -/
normedAlgebraRat : {𝕜 : Type u_6} → [inst : NormedDivisionRing 𝕜] → [CharZero 𝕜] → [NormedAlgebra ℝ 𝕜] → NormedAlgebra ℚ 𝕜
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- `c.toUnder` is a lift of `c` under the forgetful functor.  -/
CategoryTheory.Limits.Cone.mapConeToUnder : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cone F) → (CategoryTheory.Under.forget c.pt).mapCone c.toUnder ≅ c
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.nonsingularPointEquivSubtype_symm_none : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {p : W'.Point → Prop}
  (p0 : p WeierstrassCurve.Affine.Point.zero),
  (WeierstrassCurve.Affine.nonsingularPointEquivSubtype p0).symm none = ⟨WeierstrassCurve.Affine.Point.zero, p0⟩
-- Mathlib.RingTheory.Congruence.Defs
/-- The morphism into the quotient by a congruence relation  -/
RingCon.toQuotient : {R : Type u_1} → [inst : Add R] → [inst_1 : Mul R] → {c : RingCon R} → R → c.Quotient
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.dsimpLocation : Lean.Meta.Simp.Context → Lean.Meta.Simp.SimprocsArray → Lean.Elab.Tactic.Location → Lean.Elab.Tactic.TacticM Unit
-- Std.Data.ExtTreeMap.Lemmas
/-- Simpler variant of `getElem?_filterMap` when `LawfulEqCmp` is available.  -/
Std.ExtTreeMap.getElem?_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α}, (Std.ExtTreeMap.filterMap f t)[k]? = t[k]?.bind fun x => f k x
-- Mathlib.Analysis.Convex.MetricSpace
/-- **Alias** of `Convexity.continuous_convexCombPair'`.

---

When `X` is a bounded convex metric space, to check continuity of
`t ↦ f(t) • x(t) + (1 - f(t)) • y(t)` it suffices to show that `f` is continuous,
`x` is continuous away from `f(t) = 0`, and `y` is continuous away from `f(t) = 1`.  -/
Convexity.continuous_convexComboPair' : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] [BoundedSpace X]
  {T : Type u_3} [inst_4 : TopologicalSpace T] (f : T → ℝ),
  Continuous f →
    ∀ (hf0 : ∀ (t : T), 0 ≤ f t) (hf1 : ∀ (t : T), f t ≤ 1) (x y : T → X),
      ContinuousOn x (f ⁻¹' {0}ᶜ) →
        ContinuousOn y (f ⁻¹' {1}ᶜ) → Continuous fun i => Convexity.convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.instFiniteHomModuleCatObjIsFG : ∀ (K : Type u) [inst : Field K] (V W : FGModuleCat K), Module.Finite K (V.obj ⟶ W.obj)
-- Mathlib.Topology.MetricSpace.Bounded
Metric.tendsto_dist_right_atTop_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] (c : α) {f : β → α} {l : Filter β},
  Filter.Tendsto (fun x => dist (f x) c) l Filter.atTop ↔ Filter.Tendsto f l (Bornology.cobounded α)
-- Std.Internal.Do.WP.Frame
/-- If `wp` is built as `PreservesSup.frameClosure op` over a base post-transformer `f x E` (the frame
rule internalized into `wp`), then every program frames every resource `F` with respect to `op`.  -/
Std.Internal.Do.WP.Frames.of_frameClosure : ∀ {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] {R : Type t}
  (op : R → Pred → Pred) [∀ (r : R), Lean.Order.PreservesSup (op r)] (comp : R → R → R),
  (∀ (r r' : R) (a : Pred), op (comp r r') a = op r (op r' a)) →
    ∀ {x : Prog} {F : R},
      (∃ f,
          ∀ (x : Prog) (Q : Value → Pred) (E : EPred),
            Std.Internal.Do.wp x Q E = Lean.Order.PreservesSup.frameClosure op (f x E) Q) →
        Std.Internal.Do.WP.Frames op x F
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.of_algEquiv : ∀ {R : Type u_6} [inst : CommSemiring R] {K : Type u_7} {L : Type u_8} [inst_1 : CommSemiring K] [inst_2 : Algebra R K]
  [inst_3 : CommSemiring L] [inst_4 : Algebra R L] [h : IsFractionRing R K] (e : K ≃ₐ[R] L), IsFractionRing R L
-- Std.Data.HashMap.Lemmas
Std.HashMap.beq_iff_equiv : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : BEq β] [LawfulBEq α]
  [LawfulBEq β], (m₁ == m₂) = true ↔ m₁.Equiv m₂
-- Mathlib.Order.CompleteLattice.Defs
CompleteLinearOrder.toSDiff : {α : Type u_8} → [self : CompleteLinearOrder α] → SDiff α
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.empty_toList : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B},
  HNNExtension.NormalWord.empty.toList = []
-- Mathlib.Algebra.Homology.HomologySequence
CategoryTheory.ShortComplex.ShortExact.δ.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j), hS.δ i j hij = hS.δ i j hij
-- Mathlib.Data.Nat.Factorization.Basic
/-- The factorization of `m` in `n` is the number of positive natural numbers `i` such that `m ^ i`
divides `n`. Note `m` is prime. This set is expressed by filtering `Ico 1 b` where `b` is any bound
greater than `log m n`.  -/
Nat.factorization_eq_card_pow_dvd_of_lt : ∀ {b m n : ℕ}, Nat.Prime m → 0 < n → n < m ^ b → n.factorization m = {i ∈ Finset.Ico 1 b | m ^ i ∣ n}.card
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.ofHom_id : ∀ {M : Type u} [inst : Mul M], MagmaCat.ofHom (MulHom.id M) = CategoryTheory.CategoryStruct.id (MagmaCat.of M)
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {H : J.OneHypercoverFamily} {P : CategoryTheory.Functor Cᵒᵖ A}
  (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) {X : C}
  {S : CategoryTheory.Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S)
  (F : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index ⟨S, ⋯⟩ P)) (i : E.I₀),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift hP hE le F) (P.map (E.f i).op) =
    F.ι { Y := E.X i, f := E.f i, hf := ⋯ }
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : IsLocalRing R] [IsDomain R] (ϖ : R),
  ϖ ≠ 0 → IsLocalRing.maximalIdeal R = Ideal.span {ϖ} → Irreducible ϖ
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq_spec_5 : ∀ (x x_1 : Lean.Grind.IntInterval),
  (∀ (a a_1 b b_1 : ℤ), x = Lean.Grind.IntInterval.co a a_1 → x_1 = Lean.Grind.IntInterval.co b b_1 → False) →
    (∀ (a b : ℤ), x = Lean.Grind.IntInterval.ci a → x_1 = Lean.Grind.IntInterval.ci b → False) →
      (∀ (a b : ℤ), x = Lean.Grind.IntInterval.io a → x_1 = Lean.Grind.IntInterval.io b → False) →
        (x = Lean.Grind.IntInterval.ii → x_1 = Lean.Grind.IntInterval.ii → False) → (x == x_1) = false
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_of_contains_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β k}, (t.insertIfNew k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Mathlib.Order.Hom.Basic
OrderHom.prodIso_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (f : α →o β × γ), OrderHom.prodIso f = (OrderHom.fst.comp f, OrderHom.snd.comp f)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.dist_self : ∀ {α : Type u} [self : PseudoMetricSpace α] (x : α), dist x x = 0
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_top : ∀ {R : Type u_2} [inst : NonAssocRing R], ⊤.unop = ⊤
-- Lean.Elab.Util
_private.Lean.Elab.Util.0.Lean.Elab.mkUnusedBaseName.loop : Lean.Name → Lean.Name → ℕ → Lean.MacroM Lean.Name
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiffWithinAt_finsetSum`. -/
contMDiffWithinAt_finset_sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι}
  {f : ι → M → G},
  (∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) → ContMDiffWithinAt I' I n (fun x => ∑ i ∈ t, f i x) s x
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.bracketedOption : Lean.ParserDescr
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.mul_eq_comp : ∀ {𝕜₂ : Type u_6} {F : Type u_10} [inst : NormedField 𝕜₂] [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] (f g : F →WOT[𝕜₂] F), f * g = f.comp g
-- Std.Data.ExtDHashMap.Basic
/-- Checks whether a key is present in a map and inserts a value for the key if it was not found.

If the returned `Bool` is `true`, then the returned map is unaltered. If the `Bool` is `false`, then
the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `contains` followed by `insertIfNew`.
 -/
Std.ExtDHashMap.containsThenInsertIfNew : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [EquivBEq α] → [LawfulHashable α] → Std.ExtDHashMap α β → (a : α) → β a → Bool × Std.ExtDHashMap α β