mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.ProveEq
/-- Try to construct a proof that `lhs = rhs` using the information in the
goal state. If `lhs` and `rhs` have not been internalized, this function
will internalize then, process propagated equalities, and then check
whether they are in the same equivalence class or not.
The goal state is not modified by this function.
This function mainly relies on congruence closure, and constraint
propagation. It will not perform case analysis.
 -/
Lean.Meta.Grind.proveEq? : Lean.Expr → Lean.Expr → optParam Bool false → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
_private.Mathlib.AlgebraicTopology.SimplicialSet.Degenerate.0.SSet.unique_nonDegenerate.g.eq_1 : ∀ {n m₁ m₂ : ℕ} {f₁ : { len := n } ⟶ { len := m₁ }} (hf₁ : CategoryTheory.SplitEpi f₁)
  (f₂ : { len := n } ⟶ { len := m₂ }),
  SSet.unique_nonDegenerate.g✝ hf₁ f₂ = CategoryTheory.CategoryStruct.comp hf₁.section_ f₂
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.length_toList : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.HasSize α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_6 : Std.Rxc.IsAlwaysFinite α] [Std.Rxc.LawfulHasSize α], r.toList.length = r.size
-- Mathlib.Lean.Meta
/-- Implementation of `intros!`.  -/
_private.Mathlib.Lean.Meta.0.Lean.MVarId.intros!.run : Lean.MVarId → Array Lean.FVarId → Lean.MVarId → Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- A Dirichlet character `χ` factors through `d | n` iff its associated unit-group hom is trivial
on the kernel of `ZMod.unitsMap`.  -/
DirichletCharacter.factorsThrough_iff_ker_unitsMap : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} {d : ℕ} [NeZero n] (hd : d ∣ n),
  χ.FactorsThrough d ↔ (ZMod.unitsMap hd).ker ≤ (MulChar.toUnitHom χ).ker
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.equiv_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
  TopologicalSpace.Compacts.equiv f.symm = (TopologicalSpace.Compacts.equiv f).symm
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.orderTop_single : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {a : Γ} {r : R},
  r ≠ 0 → ((HahnSeries.single a) r).orderTop = ↑a
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.leftOp_functor_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ Dᵒᵖ) {X Y : Cᵒᵖ} (f : X ⟶ Y), e.leftOp.functor.map f = (e.functor.map f.unop).unop
-- Mathlib.Data.Vector.Defs
/-- Vector is determined by the underlying list.  -/
List.Vector.eq : ∀ {α : Type u_1} {n : ℕ} (a1 a2 : List.Vector α n), a1.toList = a2.toList → a1 = a2
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
/-- The shifted boundary map of the resolution.  -/
TopRep.resolution'd : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] →
      [inst_1 : Group G] →
        [inst_2 : TopologicalSpace k] →
          [inst_3 : TopologicalSpace G] →
            [inst_4 : IsTopologicalGroup G] → (X : TopRep k G) → (n : ℕ) → X.resolution'X n ⟶ X.resolution'X (n + 1)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.erase_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M), MonoidAlgebra.erase m 0 = 0
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The base machine state space is a pair of an `Option Stmt₁` representing the current program
to be executed, or `none` for the halt state, and a `σ` which is the local state (stored in the TM,
not the tape). Because there are an infinite number of programs, this state space is infinite, but
for a finitely supported TM1 machine and a finite type `σ`, only finitely many of these states are
reachable.  -/
Turing.TM1to0.Λ' : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → (Λ → Turing.TM1.Stmt Γ Λ σ) → Type (max (max (max u_3 u_2) u_1) u_3)
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Martingale.smul : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] (c : ℝ),
  MeasureTheory.Martingale f ℱ μ → MeasureTheory.Martingale (c • f) ℱ μ
-- Mathlib.ModelTheory.ElementarySubstructures
/-- The closure of a set meeting definable sets is an elementary substructure.  -/
FirstOrder.Language.MeetsDefinable.isElementary_closure : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {A : Set M},
  FirstOrder.Language.MeetsDefinable A → ((FirstOrder.Language.Substructure.closure L).toFun A).IsElementary
-- Init.Data.BitVec.Basic
/-- Returns the `i`th least significant bit or `false` if `i ≥ w`.  -/
BitVec.getLsbD : {w : ℕ} → BitVec w → ℕ → Bool
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.isSameSolverTerms : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms → Bool
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderivWithin_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 c s x →
      DifferentiableWithinAt 𝕜 f s x →
        fderivWithin 𝕜 (c • f) s x = c x • fderivWithin 𝕜 f s x + (fderivWithin 𝕜 c s x).smulRight (f x)
-- Mathlib.Topology.Constructions
set_pi_mem_nhds : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {i : Set ι} {s : (a : ι) → Set (A a)}
  {x : (a : ι) → A a}, i.Finite → (∀ a ∈ i, s a ∈ nhds (x a)) → i.pi s ∈ nhds x
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
SSet.ιChainComplex.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n })),
  X.ιChainComplex x = CategoryTheory.Limits.Sigma.ι (fun x => R) x
-- Init.Notation
/-- Specify a library suggestion engine.
Note that Lean does not ship a default library suggestion engine,
so this is only useful in conjunction with a downstream package which provides one.
 -/
Lean.setLibrarySuggestionsCmd : Lean.ParserDescr
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A CW complex has weak topology, i.e. a set `A` in `X` is closed iff its intersection with
every closed cell is closed. Use `CWComplex.closed` instead.  -/
Topology.CWComplex.closed' : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} [self : Topology.CWComplex C],
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : Topology.CWComplex.cell C n),
        IsClosed (A ∩ ↑(Topology.CWComplex.map n j) '' Metric.closedBall 0 1)) →
      IsClosed A
-- Mathlib.RingTheory.TensorProduct.Maps
/-- `S`-linear version of `Algebra.TensorProduct.comm` when `A ⊗[R] S`
is viewed as an `S`-algebra via the right component.  -/
Algebra.TensorProduct.commRight : (R : Type uR) →
  (S : Type uS) →
    (A : Type uA) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] →
            [inst_3 : Semiring A] → [inst_4 : Algebra R A] → TensorProduct R S A ≃ₐ[S] TensorProduct R A S
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- A precoverage is stable under `⊔` if whenever `R` and `S` are coverings,
also `R ⊔ S` is a covering.  -/
CategoryTheory.Precoverage.IsStableUnderSup : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Precoverage C → Prop
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.liftCocycle.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α α_1 : CochainComplex.HomComplex.Cocycle M K n) (e_α : α = α_1)
  (β β_1 : CochainComplex.HomComplex.Cochain M L m) (e_β : β = β_1) (h : m + 1 = n)
  (hαβ : CochainComplex.HomComplex.δ m n β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0),
  CochainComplex.mappingCocone.liftCocycle φ α β h hαβ = CochainComplex.mappingCocone.liftCocycle φ α_1 β_1 h ⋯
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- If `IsCyclotomicExtension {n} K L`, then `L` is the splitting field of `cyclotomic n K`.  -/
IsCyclotomicExtension.splitting_field_cyclotomic : ∀ (n : ℕ) [NeZero n] (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [IsCyclotomicExtension {n} K L], Polynomial.IsSplittingField K L (Polynomial.cyclotomic n K)
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.inter : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X},
  Topology.IsLocallyConstructible s → Topology.IsLocallyConstructible t → Topology.IsLocallyConstructible (s ∩ t)
-- Lean.MetavarContext
/-- Metavariable declarations.  -/
Lean.MetavarContext.decls : Lean.MetavarContext → Lean.PersistentHashMap Lean.MVarId Lean.MetavarDecl
-- Mathlib.Combinatorics.Graph.Lattice
Graph.inf_isNonloopAt_iff : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β},
  (G ⊓ H).IsNonloopAt e x ↔ ∃ y, y ≠ x ∧ G.IsLink e x y ∧ H.IsLink e x y
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.X_inj : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [Nontrivial R] {s t : σ},
  MvPowerSeries.X s = MvPowerSeries.X t ↔ s = t
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.lie_eq_bot_iff : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  (I : LieIdeal R L), ⁅I, N⁆ = ⊥ ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0
-- Mathlib.Algebra.Group.Defs
InvolutiveInv.toInv : {G : Type u_2} → [self : InvolutiveInv G] → Inv G
-- Mathlib.RingTheory.HopfAlgebra.Basic
HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit : ∀ {R : Type u} {A : Type v} {ι : Type u_1} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A]
  {a : A} (repr : Coalgebra.Repr R a ι),
  ∑ i ∈ repr.index, repr.left i * (HopfAlgebraStruct.antipode R) (repr.right i) =
    (algebraMap R A) (CoalgebraStruct.counit a)
-- Mathlib.Tactic.Linarith.Frontend
/-- Run the core `linarith` procedure on the goal `g` using the hypotheses `hyps`.
If `only_on` is true, the search is restricted to `hyps`; otherwise all suitable
local hypotheses are considered. This is the workhorse behind the user-facing
`linarith` tactic.
 -/
Mathlib.Tactic.Linarith.linarith : Bool → List Lean.Expr → optParam Mathlib.Tactic.Linarith.LinarithConfig { } → Lean.MVarId → Lean.MetaM Unit
-- Mathlib.Algebra.Ring.NonZeroDivisors
IsRightRegular.isUnit_of_finite : ∀ {R : Type u_1} [inst : Monoid R] {r : R} [Finite R], IsRightRegular r → IsUnit r
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend_d_from_eq_zero : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' j' : ι')
  (i : ι), e.f i = i' → ¬c.Rel i (c.next i) → (K.extend e).d i' j' = 0
-- Mathlib.Tactic.Choose
Mathlib.Tactic.Choose.instInhabitedChooseArg : Inhabited Mathlib.Tactic.Choose.ChooseArg
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.wittPolyProdRemainder.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  WittVector.wittPolyProdRemainder p n = ∑ i ∈ Finset.range n, ↑p ^ i * WittVector.wittMul p i ^ p ^ (n - i)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.smul_comp : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {S₃ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring R₃] [inst_3 : Monoid S₃] {M : Type u_6} [inst_4 : TopologicalSpace M] [inst_5 : AddCommMonoid M]
  [inst_6 : Module R M] {M₂ : Type u_7} [inst_7 : TopologicalSpace M₂] [inst_8 : AddCommMonoid M₂]
  [inst_9 : Module R₂ M₂] {M₃ : Type u_8} [inst_10 : TopologicalSpace M₃] [inst_11 : AddCommMonoid M₃]
  [inst_12 : Module R₃ M₃] [inst_13 : DistribMulAction S₃ M₃] [inst_14 : SMulCommClass R₃ S₃ M₃]
  [inst_15 : ContinuousConstSMul S₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃}
  [inst_16 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (c : S₃) (h : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂),
  (c • h) ∘SL f = c • h ∘SL f
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- A multicofork is a cocone over a multispan.  -/
CategoryTheory.Limits.Multicofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      CategoryTheory.Limits.MultispanIndex J C → Type (max (max (max w w') u) v)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function is analytic on a set `s`, so are its successive Fréchet derivative within this
set. Note that this theorem does not require completeness of the space.  -/
AnalyticOn.iteratedFDerivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E}, AnalyticOn 𝕜 f s → UniqueDiffOn 𝕜 s → ∀ (n : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s
-- Mathlib.Data.Quot
/-- A version of `Quotient.inductionOn₃` taking `{s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid γ}`
as implicit arguments instead of instance arguments.  -/
Quotient.inductionOn₃' : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid γ}
  {p : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃),
  (∀ (a₁ : α) (a₂ : β) (a₃ : γ), p (Quotient.mk'' a₁) (Quotient.mk'' a₂) (Quotient.mk'' a₃)) → p q₁ q₂ q₃
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.isLowerSet_support_singularValues : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F), IsLowerSet ↑T.singularValues.support
-- Mathlib.CategoryTheory.Equivalence.Symmetry
/-- We can compare the way we obtain a natural isomorphism `e.inverse ≅ f.inverse` from
an isomorphism `e ≌ f` via `inverseFunctor` with the way we get one through
`Iso.isoInverseOfIsoFunctor`.  -/
CategoryTheory.Equivalence.inverseFunctorMapIso_symm_eq_isoInverseOfIsoFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {e f : C ≌ D} (α : e ≅ f),
  ((CategoryTheory.Equivalence.inverseFunctor C D).mapIso α.symm).unop =
    ((CategoryTheory.Equivalence.functorFunctor C D).mapIso α).isoInverseOfIsoFunctor
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- **Alias** of `Complex.UnitDisc.star_neg`. -/
Complex.UnitDisc.conj_neg : ∀ (z : Complex.UnitDisc), star (-z) = -star z
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffAt.comp₂_contDiffWithinAt : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_6}
  {E₂ : Type u_7} [inst_5 : NormedAddCommGroup E₁] [inst_6 : NormedAddCommGroup E₂] [inst_7 : NormedSpace 𝕜 E₁]
  [inst_8 : NormedSpace 𝕜 E₂] {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : F → E₂} {s : Set F} {x : F},
  ContDiffAt 𝕜 n g (f₁ x, f₂ x) →
    ContDiffWithinAt 𝕜 n f₁ s x → ContDiffWithinAt 𝕜 n f₂ s x → ContDiffWithinAt 𝕜 n (fun x => g (f₁ x, f₂ x)) s x
-- Mathlib.Data.Countable.Defs
Function.Injective.countable : ∀ {α : Sort u} {β : Sort v} [Countable β] {f : α → β}, Function.Injective f → Countable α
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.star_mul_eq_coe : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R], star a * a = ↑(star a * a).re
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α}, (List.map Prod.fst l).contains k = false → (Std.HashMap.Raw.ofList l)[k]? = none
-- Mathlib.Order.SuccPred.Limit
/-- A value can be built by building it on maximal elements, predecessors,
and predecessor limits.  -/
Order.isPredLimitRecOn : {α : Type u_1} →
  (b : α) →
    {motive : α → Sort u_2} →
      [inst : PartialOrder α] →
        [inst_1 : PredOrder α] →
          ((a : α) → IsMax a → motive a) →
            ((a : α) → ¬IsMin a → motive (Order.pred a)) → ((a : α) → Order.IsPredLimit a → motive a) → motive b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.Key.mk.injEq : ∀ (w : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w) (w_1 : ℕ) (expr_1 : Std.Tactic.BVDecide.BVExpr w_1),
  ({ w := w, expr := expr } = { w := w_1, expr := expr_1 }) = (w = w_1 ∧ expr ≍ expr_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.flip_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (t : CategoryTheory.Limits.PullbackCone f g), t.flip.fst = t.snd
-- Mathlib.Topology.Separation.Regular
Topology.IsInducing.completelyNormalSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompletelyNormalSpace Y]
  {e : X → Y}, Topology.IsInducing e → CompletelyNormalSpace X
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenCoendFunctor_obj : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)),
  CategoryTheory.Limits.chosenCoendFunctor.obj F = CategoryTheory.Limits.chosenCoend F
-- Lean.Meta.Tactic.Simp.Types
/-- Returns `true` if `simp` is in `dsimp` mode.
That is, only transformations that preserve definitional equality should be applied.
 -/
Lean.Meta.Simp.inDSimp : Lean.Meta.SimpM Bool
-- Mathlib.Algebra.Star.SelfAdjoint
IsStarNormal.one_add : ∀ {R : Type u_1} [inst : NonAssocSemiring R] [inst_1 : StarRing R] {a : R} [ha : IsStarNormal a], IsStarNormal (1 + a)
-- Mathlib.Lean.FoldEnvironment
/-- Fold through all constants of the current file using `act`.  -/
Lean.Meta.foldCurrFileDecls : {α : Type} →
  α →
    Lean.Meta.Config → (α → Lean.Name → Lean.ConstantInfo → Lean.MetaM α) → Lean.CoreM (α × Lean.Meta.FoldDeclErrorRef)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.mk.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (asIdeal asIdeal_1 : Ideal R) (e_asIdeal : asIdeal = asIdeal_1)
  (isPrime : asIdeal.IsPrime) (ne_bot : asIdeal ≠ ⊥),
  { asIdeal := asIdeal, isPrime := isPrime, ne_bot := ne_bot } = { asIdeal := asIdeal_1, isPrime := ⋯, ne_bot := ⋯ }
-- Mathlib.Tactic.UnsetOption
/-- unset the given option name  -/
_private.Mathlib.Tactic.UnsetOption.0.Lean.Elab.elabUnsetOption.unsetOption : {m : Type → Type} → [Monad m] → [Lean.MonadOptions m] → Lean.Name → m Lean.Options
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a fallback : α},
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → Std.Internal.List.getKeyD a l fallback = Std.Internal.List.getKeyD a l' fallback
-- Lean.Meta.Tactic.Grind.AC.PP
Lean.Meta.Grind.AC.pp? : Lean.Meta.Grind.Goal → Lean.MetaM (Option Lean.MessageData)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_biUnion_finset : ∀ {α : Type u_1} {ι : Type u_3} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset ι} {f : ι → Set α},
  (↑s).PairwiseDisjoint f →
    (∀ b ∈ s, MeasurableSet (f b)) →
      autoParam (∀ b ∈ s, μ (f b) ≠ ⊤) MeasureTheory.measureReal_biUnion_finset._auto_1 →
        μ.real (⋃ b ∈ s, f b) = ∑ p ∈ s, μ.real (f p)
-- Init.Data.List.Attach
List.attachWith_ne_nil_iff : ∀ {α : Type u_1} {l : List α} {P : α → Prop} {H : ∀ a ∈ l, P a}, l.attachWith P H ≠ [] ↔ l ≠ []
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_alter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)},
  (m.alter k f).isEmpty = ((m.isEmpty || m.size == 1 && m.contains k) && (f (m.get? k)).isNone)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.instFintypeOfDecidableEqOfDecidableRelAdj : {V : Type u} → {G : SimpleGraph V} → [DecidableEq V] → [Fintype V] → [DecidableRel G.Adj] → Fintype G.Subgraph
-- Mathlib.Topology.Sheaves.Skyscraper
germ_skyscraperPresheafStalkOfSpecializes_hom : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] (A : C) [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {y : ↑X} (h : p₀ ⤳ y) (U : TopologicalSpace.Opens ↑X) (hU : y ∈ U),
  CategoryTheory.CategoryStruct.comp ((skyscraperPresheaf p₀ A).germ U y hU)
      (skyscraperPresheafStalkOfSpecializes p₀ A h).hom =
    CategoryTheory.eqToHom ⋯
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If `g` and `h` commute, then `g` fixes `h • x` iff `g` fixes `x`.
This is equivalent to say that the set `fixedBy α g` is fixed by `h`.
 -/
MulAction.fixedBy_mem_fixedBy_of_commute : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g h : G},
  Commute g h → MulAction.fixedBy α g ∈ MulAction.fixedBy (Set α) h
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.FinMeasSupp.of_lintegral_ne_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ENNReal},
  f.lintegral μ ≠ ⊤ → f.FinMeasSupp μ
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffOn_inv : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {n : WithTop ℕ∞}, ContDiffOn 𝕜 n Inv.inv {0}ᶜ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem : ∀ {K : Type u_1} [inst : Field K] {s : Set { w // w.IsReal }} (x : NumberField.mixedEmbedding.mixedSpace K)
  {w : { w // w.IsReal }}, w ∉ s → ((NumberField.mixedEmbedding.negAt s) x).1 w = x.1 w
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.pi_le_four : Real.pi ≤ 4
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.mul_edgeDensity_le_edgeDensity : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] {s₁ s₂ : Finset α}
  {t₁ t₂ : Finset β},
  s₂ ⊆ s₁ →
    t₂ ⊆ t₁ →
      s₂.Nonempty →
        t₂.Nonempty → ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card) * Rel.edgeDensity r s₂ t₂ ≤ Rel.edgeDensity r s₁ t₁
-- Mathlib.Algebra.Order.Group.MinMax
min_neg_neg : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b : α),
  min (-a) (-b) = -max a b
-- Init.Data.Array.Find
/-- `xs.findIdx p = i` iff `p xs[i]` and `¬ p xs [j]` for all `j < i`.  -/
Array.findIdx_eq : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} {i : ℕ} (h : i < xs.size),
  Array.findIdx p xs = i ↔ p xs[i] = true ∧ ∀ (j : ℕ) (hji : j < i), p xs[j] = false
-- Lean.LoadDynlib
/-- A reference to a symbol within a dynamic library.  -/
Lean.Dynlib.Symbol : Lean.Dynlib → Type
-- Mathlib.RingTheory.Nilpotent.Defs
Commute.isNilpotent_mul_right : ∀ {R : Type u_1} {x y : R} [inst : Semiring R], Commute x y → IsNilpotent x → IsNilpotent (x * y)