mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Internal.Order.Basic
/-- The fixpoint induction theme: An admissible predicate holds for a least fixpoint if it is preserved
by the fixpoint's function.

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
Lean.Order.fix_induct : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] {f : α → α} (hf : Lean.Order.monotone f) (motive : α → Prop),
  Lean.Order.admissible motive → (∀ (x : α), motive x → motive (f x)) → motive (Lean.Order.fix f hf)
-- Mathlib.Data.List.Duplicate
List.Duplicate.mem : ∀ {α : Type u_1} {l : List α} {x : α}, List.Duplicate x l → x ∈ l
-- Mathlib.Order.Interval.Set.OrdConnectedLinear
/-- A version of `Set.Nonempty.ordConnected_iff_of_bdd` for complete linear orders, such as `Fin n`,
in which the explicit boundedness hypotheses are not necessary.  -/
Set.Nonempty.ordConnected_iff_of_bdd' : ∀ {α : Type u_1} {I : Set α} [inst : ConditionallyCompleteLinearOrder α] [OrderTop α] [OrderBot α]
  [LocallyFiniteOrder α], I.Nonempty → (I.OrdConnected ↔ I = Set.Icc (sInf I) (sSup I))
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_inter_distrib_right : ∀ {α : Type u_1} (s t r : Set α), (t ∩ r) \ s = t \ s ∩ (r \ s)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isEmpty_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)}, (t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.Algebra.Algebra.Hom
AlgHomClass.mk : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : FunLike F A B]
  [toRingHomClass : RingHomClass F A B],
  (∀ (f : F) (r : R), f ((algebraMap R A) r) = (algebraMap R B) r) → AlgHomClass F R A B
-- Aesop.Tree.Data
Aesop.Goal.setIsForcedUnprovable : Bool → Aesop.Goal → Aesop.Goal
-- Lean.Util.RecDepth
Lean.maxRecDepth : Lean.Option ℕ
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.functorOfPredicateSet_map : ∀ {α : PartOrdEmb} (P : Set ↑α → Prop) {X Y : Subtype P} (f : X ⟶ Y),
  (PartOrdEmb.functorOfPredicateSet P).map f =
    PartOrdEmb.ofHom { toFun := fun x => ⟨↑x, ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ }
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.SavedState.restore : Lean.Elab.Tactic.SavedState → optParam Bool false → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Tactic.ClickSuggestions.TryPremises
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.grw.sizeOf_spec : ∀ (i : Mathlib.Tactic.ClickSuggestions.GrwInfo) (arr : Array Mathlib.Tactic.ClickSuggestions.GrwLemma),
  sizeOf (Mathlib.Tactic.ClickSuggestions.Candidates.grw✝ i arr) = 1 + sizeOf i + sizeOf arr
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.norm.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.norm c = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.norm c_1) = (c = c_1)
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.continuousLinearMapOfBilin_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E], InnerProductSpace.continuousLinearMapOfBilin 0 = 0
-- Mathlib.Order.WithBot
WithBot.instUniqueOfIsEmpty : {α : Type u_1} → [IsEmpty α] → Unique (WithBot α)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.lift_mk'_spec : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  (hg : ∀ (y : ↥M), IsUnit (g ↑y)) (x : R) (v : P) (y : ↥M),
  (IsLocalization.lift hg) (IsLocalization.mk' S x y) = v ↔ g x = g ↑y * v
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_eq_one : ∀ (α : Type u) [Subsingleton α] [Nonempty α], Cardinal.mk α = 1
-- Init.System.IOError
IO.Error.invalidArgument.injEq : ∀ (filename : Option String) (osCode : UInt32) (details : String) (filename_1 : Option String) (osCode_1 : UInt32)
  (details_1 : String),
  (IO.Error.invalidArgument filename osCode details = IO.Error.invalidArgument filename_1 osCode_1 details_1) =
    (filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1)
-- Mathlib.Topology.Category.LightProfinite.Extend
/-- Given a sequential cone in `LightProfinite` consisting of finite sets,
we obtain a functor from the opposite of the indexing category to
`CostructuredArrow toProfinite.op ⟨c.pt⟩`.
 -/
LightProfinite.Extend.functorOp : {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} →
  (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) →
    CategoryTheory.Functor ℕ (CategoryTheory.CostructuredArrow FintypeCat.toLightProfinite.op (Opposite.op c.pt))
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_neg : ∀ (x y : ℂ), x ^ (-y) = (x ^ y)⁻¹
-- Lean.Util.ParamMinimizer
/-- **Runs the parameter minimization procedure.**

Given an initial bitmask `initialMask` representing the active parameters,
and a monotonic predicate `test : Array Bool → m Bool`, this function searches
for the smallest (1-minimal) superset of `initialMask` that satisfies `test`.

Execution proceeds in two phases:

1. **`init`** – gradually activates parameters until `test` first succeeds;
2. **`prune`** – removes superfluous active parameters while preserving success.

If the search completes without exceeding `maxCalls`, the result is marked as
`.precise`.  If the budget is exceeded but a valid configuration was found,
the result is `.approx`.  If no configuration satisfies `test`, the result is
`.missing`.

`maxCalls = 0` disables the call budget limit.
 -/
Lean.Util.ParamMinimizer.search : {m : Type → Type} → [Monad m] → Array Bool → (Array Bool → m Bool) → optParam ℕ 0 → m Lean.Util.ParamMinimizer.Result
-- Mathlib.Logic.Equiv.Prod
/-- Product of two equivalences, in terms of `PProd`. If `α ≃ β` and `γ ≃ δ`, then
`PProd α γ ≃ PProd β δ`.  -/
Equiv.pprodCongr : {α : Sort u_1} → {β : Sort u_4} → {γ : Sort u_7} → {δ : Sort u_8} → α ≃ β → γ ≃ δ → α ×' γ ≃ β ×' δ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} {h' : k ∈ Std.DTreeMap.Raw.filter f t} (h : t.WF),
  Std.DTreeMap.Raw.Const.get (Std.DTreeMap.Raw.filter f t) k h' = Std.DTreeMap.Raw.Const.get t k ⋯
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.ofCoeff_zero : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M], { coeff := 0 } = 0
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.StAct.push.inj : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} {a a_1 : σ → Γ k},
  Turing.TM2to1.StAct.push a = Turing.TM2to1.StAct.push a_1 → a = a_1
-- Mathlib.Order.Lattice
inf_idem : ∀ {α : Type u} [inst : SemilatticeInf α] (a : α), a ⊓ a = a
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_ext_right_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {f : J → C} {X Y : C}
  {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) Y},
  g = h ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp g
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) =
        CategoryTheory.CategoryStruct.comp h
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y)
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.GuessLexRel.ofNat : ℕ → Lean.Elab.WF.GuessLex.GuessLexRel
-- Mathlib.Algebra.Ring.NonZeroDivisors
isRegular_iff_isUnit_of_finite : ∀ {R : Type u_1} [inst : Monoid R] {r : R} [Finite R], IsRegular r ↔ IsUnit r
-- Mathlib.Algebra.Order.Monovary
antivary_iff_forall_mul_nonpos : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α},
  Antivary f g ↔ ∀ (i j : ι), (f j - f i) * (g j - g i) ≤ 0
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim : ∀ (R : Type u) [inst : CommSemiring R], topologicalKrullDim (PrimeSpectrum R) = ringKrullDim R
-- Init.Data.UInt.Lemmas
UInt8.zero_ne_one : 0 ≠ 1
-- Mathlib.RingTheory.Finiteness.Prod
Module.Finite.prod : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [hM : Module.Finite R M] [hN : Module.Finite R N],
  Module.Finite R (M × N)
-- Mathlib.Order.Filter.Bases.Basic
FilterBasis.eq_iInf_principal : ∀ {α : Type u_1} (B : FilterBasis α), B.filter = ⨅ s, Filter.principal ↑s
-- Mathlib.Topology.Connected.LocallyConnected
IsOpen.connectedComponentIn : ∀ {α : Type u} [inst : TopologicalSpace α] [LocallyConnectedSpace α] {F : Set α} {x : α},
  IsOpen F → IsOpen (connectedComponentIn F x)
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.hilbertPoly_zero_right : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F), p.hilbertPoly 0 = 0
-- Mathlib.NumberTheory.ModularForms.Bounds
/-- **Hecke's bound** for the coefficients of a cusp form: if `f` is a weight `k` modular form for
an arithmetic subgroup, then its `q`-expansion coefficients are `O (n ^ (k / 2))`.

This is not optimal -- the optimal exponent is `(k - 1) / 2 + ε` for any `0 < ε`, at least for
congruence levels -- but is much easier to prove than the optimal result.  -/
CuspFormClass.qExpansion_isBigO : ∀ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_2} [inst : FunLike F UpperHalfPlane ℂ]
  [CuspFormClass F Γ k] (f : F),
  (fun n => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f)) =O[Filter.atTop] fun n =>
    ↑n ^ (↑k / 2)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.coloops_subset_ground : ∀ {α : Type u_1} (M : Matroid α), M.coloops ⊆ M.E
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.uniqueOfLeft : {R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {M : Type u_8} →
      {M₂ : Type u_10} →
        [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₂} → [Subsingleton M] → Unique (M →ₛₗ[σ₁₂] M₂)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.comp_left : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [inst_6 : CategoryTheory.Category.{v₇, u₇} A'']
  [inst_7 : CategoryTheory.Category.{v₈, u₈} B''] [inst_8 : CategoryTheory.Category.{v₉, u₉} C'']
  {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''}
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G')
  (ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''), (ψ.comp ψ').left = ψ.left.comp ψ'.left
-- Mathlib.Algebra.Ring.Int.Parity
Int.even_mul_pred_self : ∀ (n : ℤ), Even (n * (n - 1))
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.homothety_zero : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1), AffineMap.homothety c 0 = AffineMap.const k P1 c
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof : Type
-- Lean.Meta.Tactic.Simp.Types
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.mkCongrSimp?.go? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Meta.CongrTheorem)
-- Mathlib.GroupTheory.Perm.List
List.formPerm_apply_getLast : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α) (xs : List α), (x :: xs).formPerm ((x :: xs).getLast ⋯) = x
-- Mathlib.Order.GaloisConnection.Basic
sInf_image2_eq_sInf_sSup : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (u₁ b) (Function.swap u b)) →
    (∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) →
      sInf (Set.image2 u s t) = u (sInf s) (sSup t)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The structure of two-sided continuous isomorphisms between groups.
Note that both the map and its inverse have to be continuous.  -/
«term_≃ₜ*_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.rpow_neg_one_le_one : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {a : A},
  1 ≤ a → a ^ (-1) ≤ 1
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.sdiff_nonempty_of_ncard_lt_ncard`. -/
Set.diff_nonempty_of_ncard_lt_ncard : ∀ {α : Type u_1} {s t : Set α},
  s.ncard < t.ncard → autoParam s.Finite Set.sdiff_nonempty_of_ncard_lt_ncard._auto_1 → (t \ s).Nonempty
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_one : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (n : σ), MvPolynomial.degreeOf n 1 = 0
-- Lean.Data.JsonRpc
Lean.JsonRpc.instCoeOutNotificationMessageOfToJson : {α : Type u_1} → [Lean.ToJson α] → CoeOut (Lean.JsonRpc.Notification α) Lean.JsonRpc.Message
-- Mathlib.Analysis.Normed.Module.Basic
instNonUnitalNormedCommRingRestrictScalars : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} → {E : Type u_3} → [I : NonUnitalNormedCommRing E] → NonUnitalNormedCommRing (RestrictScalars 𝕜 𝕜' E)
-- Aesop.Search.Expansion.Norm
Aesop.NormM.State : Type
-- Lean.Environment
/-- Bumps all modules' `isExported` flag to true, intended for use in `shake` only.  -/
Lean.ImportState.markAllExported : Lean.ImportState → Lean.ImportState
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.isGreatest_ofFunction : ∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0},
  IsGreatest {μ | ∀ (s : Set α), μ s ≤ m s} (MeasureTheory.OuterMeasure.ofFunction m m_empty)
-- Mathlib.Topology.Homotopy.Lifting
/-- The abstract monodromy theorem: if `γ₀` and `γ₁` are two paths in a topological space `X`,
`γ` is a homotopy between them relative to the endpoints, and the path at each time step of
the homotopy, `γ (t, ·)`, lifts to a continuous path `Γ t` through a separated local
homeomorphism `p : E → X`, starting from some point in `E` independent of `t`. Then the
endpoints of these lifts are also independent of `t`.

This can be applied to continuation of analytic functions as follows: for a sheaf of analytic
functions on an analytic manifold `X`, we may consider its étale space `E` (whose points are
analytic germs) with the natural projection `p : E → X`, which is a local homeomorphism and a
separated map (because two analytic functions agreeing on a nonempty open set agree on the
whole connected component). An analytic continuation of a germ along a path `γ (t, ·) : C(I, X)`
corresponds to a continuous lift of `γ (t, ·)` to `E` starting from that germ. If `γ` is a
homotopy and the germ admits continuation along every path `γ (t, ·)`, then the result of the
continuations are independent of `t`. In particular, if `X` is simply connected and an analytic
germ at `p : X` admits a continuation along every path in `X` from `p` to `q : X`, then the
continuation to `q` is independent of the path chosen.  -/
IsLocalHomeomorph.monodromy_theorem : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X},
  IsLocalHomeomorph p →
    IsSeparatedMap p →
      ∀ {γ₀ γ₁ : C(↑unitInterval, X)} (γ : γ₀.HomotopyRel γ₁ {0, 1}) (Γ : ↑unitInterval → C(↑unitInterval, E)),
        (∀ (t s : ↑unitInterval), p ((Γ t) s) = γ (t, s)) →
          (∀ (t : ↑unitInterval), (Γ t) 0 = (Γ 0) 0) → ∀ (t : ↑unitInterval), (Γ t) 1 = (Γ 0) 1
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.tidy.injEq : ∀ {s : Lean.Omega.Constraint} {c : Lean.Omega.Coeffs} (j j_1 : Lean.Elab.Tactic.Omega.Justification s c),
  (j.tidy = j_1.tidy) = (j = j_1)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
/-- Given a type `α`, this is the functor `FormalCoproduct C ⥤ FormalCoproduct C`
which sends `U` to `U.power α`.  -/
CategoryTheory.Limits.FormalCoproduct.powerFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (α : Type t) →
      [CategoryTheory.Limits.HasProductsOfShape α C] →
        CategoryTheory.Functor (CategoryTheory.Limits.FormalCoproduct C) (CategoryTheory.Limits.FormalCoproduct C)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The addition of two nonsingular points on a Weierstrass curve in affine coordinates.

Given two nonsingular points `P` and `Q` in affine coordinates, use `P + Q` instead of `add P Q`.  -/
WeierstrassCurve.Affine.Point.add : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Affine F} → [DecidableEq F] → W.Point → W.Point → W.Point
-- Aesop.Search.Expansion.Norm
Aesop.mkNormSimpScriptStep : Lean.MVarId →
  Option Lean.MVarId →
    Lean.Meta.SavedState → Lean.Meta.SavedState → Lean.Meta.Simp.UsedSimps → Aesop.NormM Aesop.Script.LazyStep
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_diff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k fallback : α}, (m₁ \ m₂).getKeyD k fallback = if k ∈ m₂ then fallback else m₁.getKeyD k fallback
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- Construct an element of the value group-with-zero from an element `r : R` and
`y : posSubmonoid R`. This should be thought of as `v r / v y`.  -/
ValuativeRel.ValueGroupWithZero.mk : {R : Type u_1} →
  [inst : Semiring R] →
    [inst_1 : ValuativeRel R] → R → ↥(ValuativeRel.posSubmonoid R) → ValuativeRel.ValueGroupWithZero R
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.mkLabelledStar : Lean.MVarId → Lean.Meta.RefinedDiscrTree.LazyM✝ Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.Order.Antichain
IsAntichain.flip : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsAntichain r s → IsAntichain (flip r) s
-- Mathlib.Tactic.RewriteSearch
/-- `rw_search` has been removed from Mathlib.
 -/
Mathlib.Tactic.RewriteSearch.tacticRw_search_ : Lean.ParserDescr
-- Mathlib.Topology.EMetricSpace.Weak
Option.edist_self' : ∀ {α : Type u} [inst : TopologicalSpace α] (m : WeakPseudoEMetricSpace α) (x : Option α), edist x x = 0
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- The bound on the degree of the polynomials used to describe the constructible set appearing in
the case of `C : R → R[X]` of Chevalley's theorem with complexity bound.  -/
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.degBound : {R : Type u_2} → [inst : CommRing R] → {n : ℕ} → ChevalleyThm.PolynomialC.InductionObj✝ R n → ℕ
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.instNat : Lean.Elab.ConfigEval.EvalExpr ℕ
-- Mathlib.Logic.Basic
Iff.ne_left : ∀ {α : Sort u_1} {β : Sort u_2} {a b : α} {c d : β}, (a = b ↔ c ≠ d) → (a ≠ b ↔ c = d)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.is_sheafedSpace_iso : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [CategoryTheory.IsIso f],
  CategoryTheory.IsIso (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
-- Init.System.IO
IO.Process.Output.mk.injEq : ∀ (exitCode : UInt32) (stdout stderr : String) (exitCode_1 : UInt32) (stdout_1 stderr_1 : String),
  ({ exitCode := exitCode, stdout := stdout, stderr := stderr } =
      { exitCode := exitCode_1, stdout := stdout_1, stderr := stderr_1 }) =
    (exitCode = exitCode_1 ∧ stdout = stdout_1 ∧ stderr = stderr_1)
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.instIsAddLeftInvariantMeasure : ∀ {G : Type u_3} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] [inst_2 : MeasurableSpace G]
  [inst_3 : BorelSpace G] [inst_4 : FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (Module.finrank ℝ G = n)]
  (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ), ω.measure.IsAddLeftInvariant
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.abs : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommRing α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : TopologicalSpace α] [OrderTopology α] {f : ι → α}, Multipliable f → Multipliable fun x => |f x|
-- Mathlib.Topology.Order.Compact
IsCompact.exists_isLocalMin_mem_open : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIicTopology α] {f : β → α} {s t : Set β} {z : β},
  IsCompact t → s ⊆ t → ContinuousOn f t → z ∈ t → (∀ z' ∈ t \ s, f z < f z') → IsOpen s → ∃ x ∈ s, IsLocalMin f x
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.le_sSup : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {c : Set (E →ₛₗ.[σ] F)}
  (hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c) {f : E →ₛₗ.[σ] F}, f ∈ c → f ≤ LinearPMap.sSup c hc
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt64.reduceLT : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mapAlongMonoidHom_apply : ∀ {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂}
  {S₁ : ι₁ → Type u_7} {S₂ : ι₂ → Type u_8} [inst : (i : ι₁) → SetLike (S₁ i) (R₁ i)]
  [inst_1 : (j : ι₂) → SetLike (S₂ j) (R₂ j)] {B₁ : (i : ι₁) → S₁ i} {B₂ : (j : ι₂) → S₂ j} (f : ι₂ → ι₁)
  (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) [inst_2 : (i : ι₁) → Monoid (R₁ i)] [inst_3 : (i : ι₂) → Monoid (R₂ i)]
  [inst_4 : ∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)] [inst_5 : ∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)]
  (φ : (j : ι₂) → R₁ (f j) →* R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j))
  (x : RestrictedProduct (fun i => R₁ i) (fun i => ↑(B₁ i)) 𝓕₁) (j : ι₂),
  ((RestrictedProduct.mapAlongMonoidHom R₁ R₂ f hf φ hφ) x) j = (φ j) (x (f j))
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.quasiCompact_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.QuasiCompact
-- Mathlib.CategoryTheory.RegularCategory.Basic
/-- In a regular category, every morphism `f : X ⟶ Y` factors as `e ≫ m`, where `e` is the projection
map to the coequalizer of the kernel pair of `f`, and `m` is the canonical map from that
coequalizer to `Y`. In particular, `f` factors as a strong epimorphism followed by a monomorphism.
 -/
CategoryTheory.Regular.strongEpiMonoFactorisation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Regular C] → {X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.StrongEpiMonoFactorisation f
-- Mathlib.RingTheory.WittVector.IsPoly
/-- The function that is constantly one on Witt vectors is a polynomial function.  -/
WittVector.oneIsPoly : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], WittVector.IsPoly p fun x x_1 x_2 => 1
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.isOpen_iff_isLowerSet : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLowerSet α] {s : Set α},
  IsOpen s ↔ IsLowerSet s
-- Mathlib.Order.Hom.Lattice
SupHom.const.eq_1 : ∀ (α : Type u_2) {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] (b : β),
  SupHom.const α b = { toFun := fun x => b, map_sup' := ⋯ }