mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Module
/-- Given a goal which is an equality in a type `M` (with `M` an `AddCommMonoid`), parse the LHS and
RHS of the goal as linear combinations of `M`-atoms over some semiring `R`, and reduce the goal to
the respective equalities of the `R`-coefficients of each atom.

This is an auxiliary function which produces slightly awkward goals in `R`; they are later cleaned
up by the function `Mathlib.Tactic.Module.postprocess`.  -/
Mathlib.Tactic.Module.matchScalarsAux : Lean.MVarId → Mathlib.Tactic.AtomM (List Lean.MVarId)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.closedBall_disjoint_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {δ ε : ℝ},
  δ + ε < dist x y → Disjoint (Metric.closedBall x δ) (Metric.closedBall y ε)
-- Batteries.Util.Cache
Batteries.Tactic.instNonemptyCache : ∀ {α : Type}, Nonempty (Batteries.Tactic.Cache α)
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.out.eq_1 : ∀ {p n : ℕ} {R : Type u_1} [inst : CommRing R] (x : TruncatedWittVector p n R),
  x.out = { coeff := fun i => if h : i < n then TruncatedWittVector.coeff ⟨i, h⟩ x else 0 }
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
/-- `r 1` has order `n`.
 -/
DihedralGroup.orderOf_r_one : ∀ {n : ℕ}, orderOf (DihedralGroup.r 1) = n
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.derivWeierstrassP_neg : ∀ (L : PeriodPair) (z : ℂ), L.derivWeierstrassP (-z) = -L.derivWeierstrassP z
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.instFromJsonCallHierarchy : Lean.FromJson Lean.Lsp.Ipc.CallHierarchy
-- Mathlib.Data.Bool.Basic
Bool.le_and : ∀ {x y z : Bool}, x ≤ y → x ≤ z → x ≤ (y && z)
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_self_nonneg : ∀ {A : Type u_1} {E : Type u_2} {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module ℂ A}
  {inst_3 : AddCommGroup E} {inst_4 : Module ℂ E} {inst_5 : PartialOrder A} {inst_6 : SMul A E} {inst_7 : Norm A}
  {inst_8 : Norm E} [self : CStarModule A E] {x : E}, 0 ≤ inner A x x
-- Mathlib.Algebra.Group.Action.Units
Units.instFaithfulSMul : ∀ {M : Type u_3} {α : Type u_5} [inst : Monoid M] [inst_1 : SMul M α] [FaithfulSMul M α], FaithfulSMul Mˣ α
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.mk.sizeOf_spec : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] [inst_3 : SizeOf A] [inst_4 : SizeOf M] (var : relations.G → M)
  (linearCombination_var_relation : ∀ (r : relations.R), (Finsupp.linearCombination A var) (relations.relation r) = 0),
  sizeOf { var := var, linearCombination_var_relation := linearCombination_var_relation } = 1
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Monomial degree of powers  -/
MonomialOrder.degree_pow_of_pow_leadingCoeff_ne_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R} {n : ℕ},
  m.leadingCoeff f ^ n ≠ 0 → m.degree (f ^ n) = n • m.degree f
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.isClosed_cellFrontier : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] [T2Space X] {n : ℕ}
  {i : Topology.RelCWComplex.cell C n}, IsClosed (Topology.RelCWComplex.cellFrontier n i)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.any_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {p : β → Bool},
  Std.IterM.any p it = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' x => if p x = true then pure { down := true } else Std.IterM.any p it'
      | Std.IterStep.skip it' => Std.IterM.any p it'
      | Std.IterStep.done => pure { down := false }
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.coe_spanSingleton : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] (x : P), ↑(FractionalIdeal.spanSingleton S x) = R ∙ x
-- Lean.Meta.Tactic.Simp.Types
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.Context.mk.injEq : ∀ (config : Lean.Meta.Simp.Config) (userConfig : Lean.Options) (zetaDeltaSet initUsedZetaDelta : Lean.FVarIdSet)
  (metaConfig indexConfig : Lean.Meta.ConfigWithKey) (maxDischargeDepth : UInt32)
  (simpTheorems : Lean.Meta.SimpTheoremsArray) (congrTheorems : Lean.Meta.SimpCongrTheorems)
  (parent? : Option Lean.Expr) (dischargeDepth : UInt32) (lctxInitIndices : ℕ) (inDSimp : Bool)
  (config_1 : Lean.Meta.Simp.Config) (userConfig_1 : Lean.Options) (zetaDeltaSet_1 initUsedZetaDelta_1 : Lean.FVarIdSet)
  (metaConfig_1 indexConfig_1 : Lean.Meta.ConfigWithKey) (maxDischargeDepth_1 : UInt32)
  (simpTheorems_1 : Lean.Meta.SimpTheoremsArray) (congrTheorems_1 : Lean.Meta.SimpCongrTheorems)
  (parent?_1 : Option Lean.Expr) (dischargeDepth_1 : UInt32) (lctxInitIndices_1 : ℕ) (inDSimp_1 : Bool),
  ({ config := config, userConfig := userConfig, zetaDeltaSet := zetaDeltaSet, initUsedZetaDelta := initUsedZetaDelta,
        metaConfig := metaConfig, indexConfig := indexConfig, maxDischargeDepth := maxDischargeDepth,
        simpTheorems := simpTheorems, congrTheorems := congrTheorems, parent? := parent?,
        dischargeDepth := dischargeDepth, lctxInitIndices := lctxInitIndices, inDSimp := inDSimp } =
      { config := config_1, userConfig := userConfig_1, zetaDeltaSet := zetaDeltaSet_1,
        initUsedZetaDelta := initUsedZetaDelta_1, metaConfig := metaConfig_1, indexConfig := indexConfig_1,
        maxDischargeDepth := maxDischargeDepth_1, simpTheorems := simpTheorems_1, congrTheorems := congrTheorems_1,
        parent? := parent?_1, dischargeDepth := dischargeDepth_1, lctxInitIndices := lctxInitIndices_1,
        inDSimp := inDSimp_1 }) =
    (config = config_1 ∧
      userConfig = userConfig_1 ∧
        zetaDeltaSet = zetaDeltaSet_1 ∧
          initUsedZetaDelta = initUsedZetaDelta_1 ∧
            metaConfig = metaConfig_1 ∧
              indexConfig = indexConfig_1 ∧
                maxDischargeDepth = maxDischargeDepth_1 ∧
                  simpTheorems = simpTheorems_1 ∧
                    congrTheorems = congrTheorems_1 ∧
                      parent? = parent?_1 ∧
                        dischargeDepth = dischargeDepth_1 ∧ lctxInitIndices = lctxInitIndices_1 ∧ inDSimp = inDSimp_1)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_singleton_mul_right_inj : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R} [IsDomain R] {x : R},
  x ≠ 0 → (Ideal.span {x} * I = Ideal.span {x} * J ↔ I = J)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Given maps `f`, `g` from a manifold into a field `𝕜` and `𝕜`-vector space `V`, respectively, if
at some point `x`, `f` has differential `f' : TangentSpace I x →L[𝕜] 𝕜` and `g` has differential
`g' : TangentSpace I x →L[𝕜] V` (both phrased using the predicate `HasMFDerivAt`), it follows that
their scalar multiplication `f • g` has differential `f x • g' + toSpanSingleton 𝕜 (g x) ∘L f'`.

In fact, the statement above is not literally true, because, for example, the differential of `g`
really takes values in the tangent space to `V` at `g x`, rather than in `V` itself. Of course, this
tangent space can be canonically identified with `V`.

This lemma phrases the formula using the equiv `NormedSpace.fromTangentSpace`, which provides this
canonical identification. (It would also be possible to phrase the formula without this equiv,
instead using casting and definitional abuse.)  -/
_private.Mathlib.Geometry.Manifold.MFDeriv.NormedSpace.0.HasMFDerivAt.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {V : Type u_18} [inst_6 : NormedAddCommGroup V]
  [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V} {f' : TangentSpace I x →L[𝕜] 𝕜},
  HasMFDerivAt% f x (↑(NormedSpace.fromTangentSpace (f x)).symm ∘SL f') →
    ∀ {g' : TangentSpace I x →L[𝕜] V},
      HasMFDerivAt% g x (↑(NormedSpace.fromTangentSpace (g x)).symm ∘SL g') →
        HasMFDerivAt% (f • g) x
          (f x • ↑(NormedSpace.fromTangentSpace ((f • g) x)).symm ∘SL g' +
            ContinuousLinearMap.toSpanSingleton 𝕜 ((NormedSpace.fromTangentSpace ((f • g) x)).symm (g x)) ∘SL f')
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_inter_le_size_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → (m₁.inter m₂ ⋯).size ≤ m₁.size
-- Init.Data.Slice.Array.Lemmas
Subarray.toList_mkSlice_roo : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...hi) = List.drop (lo + 1) (List.take hi (Std.Slice.toList xs))
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.ofIdComp_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t :
    CategoryTheory.Bicategory.LeftLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)),
  t.ofIdComp.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor g).inv t.unit
-- Mathlib.GroupTheory.Congruence.Defs
/-- The smallest additive congruence relation containing a binary
relation `r` is contained in any additive congruence relation containing `r`.  -/
AddCon.addConGen_le : ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {c : AddCon M}, addConGen r ≤ c ↔ r ≤ ⇑c
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.AlternatingCofaceMapComplex.obj.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.CosimplicialObject C),
  AlgebraicTopology.AlternatingCofaceMapComplex.obj X =
    CochainComplex.of (fun n => X.obj { len := n }) (AlgebraicTopology.AlternatingCofaceMapComplex.objD X) ⋯
-- Lean.Elab.InfoTree.Types
/-- Indicates that an extensible document elaborator was used. This info is applied to the name on a
role, directive, code block, or command, and is used to generate the hover.

A `TermInfo` would not give the correct hover for a few reasons:
 1. The name used to invoke a document extension is not necessarily the name of the elaborator that
    was used, but the elaborator's docstring should be shown rather than that of the name as
    written.
 2. The underlying elaborator's Lean type is not an appropriate signature to show to users.
 -/
Lean.Elab.DocElabInfo : Type
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
lipschitzGroup.coe_mem_iff_mem : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ},
  ↑x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ↔ x ∈ lipschitzGroup Q
-- Mathlib.Algebra.Ring.Defs
mul_sub_right_distrib : ∀ {α : Type u} [inst : NonUnitalNonAssocRing α] (a b c : α), (a - b) * c = a * c - b * c
-- Mathlib.Order.Interval.Set.Basic
Set.mem_Ici_Ioi_of_subset_of_subset : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α} {s : Set α}, Set.Ioi a ⊆ s → s ⊆ Set.Ici a → s ∈ {Set.Ici a, Set.Ioi a}
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
cyclotomicCharacter.toFun_spec : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (p : ℕ) [inst_2 : Fact (Nat.Prime p)]
  [∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)] (g : L ≃+* L) {n : ℕ} (t : ↥(rootsOfUnity (p ^ n) L)),
  g ↑↑t = ↑↑t ^ ((PadicInt.toZModPow n) (cyclotomicCharacter.toFun p g)).val
-- Mathlib.Data.List.Basic
List.sublist_cons_of_sublist : ∀ {α : Type u} {l₁ l₂ : List α} (a : α), l₁.Sublist l₂ → l₁.Sublist (a :: l₂)
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Polynomial R}
  {a b : S}, IsUnit ((Polynomial.aeval b) P) → IsNilpotent (a - b) → IsUnit ((Polynomial.aeval a) P)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- A commutative group object internal to a Cartesian monoidal category.  -/
CategoryTheory.CommGrp : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → [CategoryTheory.BraidedCategory C] → Type (max u₁ v₁)
-- Mathlib.Topology.Compactness.Lindelof
/-- A set `s` is Lindelöf if and only if
for every open cover of `s`, there exists a countable subcover.  -/
isLindelof_iff_countable_subcover : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsLindelof s ↔
    ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getEntryₘ : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] → (m : Std.DHashMap.Internal.Raw₀ α β) → (a : α) → m.containsₘ a = true → (a : α) × β a
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of an `AddMonoid` by an additive congruence relation is
an `AddMonoid`.  -/
AddCon.addMonoid : {M : Type u_4} → [inst : AddMonoid M] → (c : AddCon M) → AddMonoid c.Quotient
-- Mathlib.Analysis.Polynomial.Factorization
/-- If `f : ℝ[X]` is monic of degree `≥ 2`, then `f = f₁ * f₂` with `f₁` monic of degree `2`
and `f₂` monic of degree `f.natDegree - 2`.

This relies on the fact that irreducible polynomials over `ℝ` have degree at most `2`.  -/
Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_two_mul_isMonicOfDegree : ∀ {f : Polynomial ℝ} {n : ℕ},
  f.IsMonicOfDegree (n + 2) → ∃ f₁ f₂, f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
-- Mathlib.Algebra.Central.Basic
Algebra.IsCentral.baseField_essentially_unique : ∀ (k : Type u_1) (K : Type u_2) (D : Type u_3) [inst : Field k] [inst_1 : Field K] [inst_2 : Ring D] [Nontrivial D]
  [inst_4 : Algebra k K] [inst_5 : Algebra K D] [inst_6 : Algebra k D] [IsScalarTower k K D] [Algebra.IsCentral k D],
  Function.Bijective ⇑(algebraMap k K)
-- Mathlib.Data.Stream.Defs
/-- `take n s` returns a list of the `n` first elements of stream `s`  -/
Stream'.take : {α : Type u} → ℕ → Stream' α → List α
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.ker_polarization_eq_ker_rootForm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι],
  P.Polarization.ker = LinearMap.ker P.RootForm
-- Init.MetaTypes
/-- When `false` (default: `true`), then disables zeta reduction of `have` expressions.
If `zeta` is `false`, then this option has no effect.
Unused `have`s are still removed if `zeta` or `zetaUnused` are true.
 -/
Lean.Meta.DSimp.Config.zetaHave : Lean.Meta.DSimp.Config → Bool
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
Std.Tactic.BVDecide.Return.mk : {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} →
  (result : aig.ExtendingEntrypoint) → Std.Tactic.BVDecide.BVExpr.Cache (↑result).aig → Std.Tactic.BVDecide.Return aig
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.coe_addEquiv : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), ⇑↑f = ⇑f
-- Mathlib.Order.Monotone.Monovary
Antivary.antivaryOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  Antivary f g → ∀ (s : Set ι), AntivaryOn f g s
-- Init.Data.Int.Gcd
Int.gcd_mul_right_right : ∀ (a b : ℤ), a.gcd (a * b) = a.natAbs
-- Mathlib.Order.Filter.Pointwise
Filter.frequently_neg_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter β} {a : α} {p : β → Prop},
  (∃ᶠ (y : β) in a +ᵥ f, p y) ↔ ∃ᶠ (x : β) in f, p (a +ᵥ x)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.id.injEq : ∀ (e : Lean.Expr) (f : Mathlib.Tactic.BicategoryLike.Mor₁) (e_1 : Lean.Expr) (f_1 : Mathlib.Tactic.BicategoryLike.Mor₁),
  (Mathlib.Tactic.BicategoryLike.StructuralAtom.id e f = Mathlib.Tactic.BicategoryLike.StructuralAtom.id e_1 f_1) =
    (e = e_1 ∧ f = f_1)
-- Mathlib.CategoryTheory.Category.Preorder
/-- A monotone function between preorders induces a functor between the associated categories.  -/
Monotone.functor : {X : Type u} →
  {Y : Type v} → [inst : Preorder X] → [inst_1 : Preorder Y] → {f : X → Y} → Monotone f → CategoryTheory.Functor X Y
-- Lean.Environment
/-- Forgets about the asynchronous context restrictions. Used only for `withoutModifyingEnv`.  -/
Lean.Environment.unlockAsync : Lean.Environment → Lean.Environment
-- Init.Data.Nat.Compare
Nat.isLE_compare : ∀ {a b : ℕ}, (compare a b).isLE = true ↔ a ≤ b
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.step_intermediateDropWhile.match_3.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Mathlib.LinearAlgebra.Dimension.Constructions
Subalgebra.rank_top : ∀ {F : Type u_2} {E : Type u_3} [inst : CommSemiring F] [inst_1 : Semiring E] [inst_2 : Algebra F E],
  Module.rank F ↥⊤ = Module.rank F E
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote_combine : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α)
  (p₁ p₂ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.Poly.denote ctx (p₁.combine p₂) =
    Lean.Grind.Linarith.Poly.denote ctx p₁ + Lean.Grind.Linarith.Poly.denote ctx p₂
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instMulOneClassOfMonoidHomClass.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → MulOneClass (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)],
  DirectLimit.instMulOneClassOfMonoidHomClass =
    { toOne := DirectLimit.instOne, toMul := DirectLimit.instMul, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Monotone.neg : ∀ {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftMono α] [AddRightMono α]
  [inst_4 : Preorder β] {f : β → α}, Monotone f → Antitone fun x => -f x
-- Mathlib.Analysis.Analytic.Composition
/-- Eta-expanded form of `AnalyticAt.comp`

---

If two functions `g` and `f` are analytic respectively at `f x` and `x`, then `g ∘ f` is
analytic at `x`.  -/
AnalyticAt.fun_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {x : E},
  AnalyticAt 𝕜 g (f x) → AnalyticAt 𝕜 f x → AnalyticAt 𝕜 (fun x => g (f x)) x
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.isUnit_leadingCoeff_mul_right_eq_zero_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, IsUnit p.leadingCoeff → ∀ {q : Polynomial R}, p * q = 0 ↔ q = 0
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_biUnion_finset_eq : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α) (t : Finset ι),
  MeasureTheory.ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, MeasureTheory.ae (μ.restrict (s i))
-- Std.Do.Triple.SpecLemmas
List.Cursor.length_suffix_le_length : ∀ {α : Type u_1} {l : List α} {c : l.Cursor}, c.suffix.length ≤ l.length
-- Mathlib.CategoryTheory.Retract
/-- If `e : X ≅ Y`, then `X` is a retract of `Y`.  -/
CategoryTheory.Retract.ofIso : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ≅ Y) → CategoryTheory.Retract X Y
-- Mathlib.Topology.ContinuousMap.Defs
/-- Deprecated. Use `map_continuous` instead.  -/
ContinuousMap.continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)), Continuous ⇑f
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.restrict.eq_1 : ∀ {K : Type u_1} [inst : Field K] {M : Type u_3} (f : M → K) (h : ∀ (x : M), IsIntegral ℤ (f x)) (x : M),
  NumberField.RingOfIntegers.restrict f h x = ⟨f x, ⋯⟩
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inl_desc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Limits.biprod.desc f g) = f
-- Mathlib.Algebra.Module.Submodule.Invariant
LinearEquiv.map_mem_invtSubmodule_conj_iff : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {f : Module.End R M} {e : M ≃ₗ[R] N} {p : Submodule R M},
  Submodule.map (↑e) p ∈ (e.conj f).invtSubmodule ↔ p ∈ f.invtSubmodule
-- Mathlib.Data.Set.Card
Finset.exists_not_mem_of_card_lt_enatCard : ∀ {α : Type u_1} {s : Finset α}, ↑s.card < ENat.card α → ∃ a, a ∉ s
-- Mathlib.Analysis.Normed.Group.NullSubmodule
mem_nullAddSubgroup_iff : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {x : M}, x ∈ nullAddSubgroup M ↔ ‖x‖ = 0
-- Mathlib.Topology.Maps.Strict.Module
/-- A linear map `f : M → N` is strict if and only if the induced map `M ⧸ f.ker → N` is an
embedding.  -/
LinearMap.isStrictMap_iff_isEmbedding_liftQ_ker : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S}
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module S N] {f : M →ₛₗ[σ] N}
  [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace N],
  Topology.IsStrictMap ⇑f ↔ Topology.IsEmbedding ⇑(f.ker.liftQ f ⋯)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Dense.extend.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} (hs : Dense s)
  (f f_1 : ↑s → β), f = f_1 → ∀ (a a_1 : α), a = a_1 → hs.extend f a = hs.extend f_1 a_1