mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Quotient.Defs
/-- The equivalence relation associated to a submodule `p`, defined by `x ≈ y` iff `-x + y ∈ p`.

Note this is equivalent to `y - x ∈ p`, but defined this way to be defeq to the `AddSubgroup`
version, where commutativity can't be assumed.  -/
Submodule.quotientRel : {R : Type u_1} →
  {M : Type u_2} → [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Submodule R M → Setoid M
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval_arithShiftRight : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {a : ℕ} {lhs : Std.Tactic.BVDecide.BVExpr a} {a_1 : ℕ}
  {rhs : Std.Tactic.BVDecide.BVExpr a_1},
  Std.Tactic.BVDecide.BVExpr.eval assign (lhs.arithShiftRight rhs) =
    (Std.Tactic.BVDecide.BVExpr.eval assign lhs).sshiftRight' (Std.Tactic.BVDecide.BVExpr.eval assign rhs)
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
CategoryTheory.GrothendieckTopology.sheafifyCompIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D), J.sheafifyCompIso F P = J.sheafifyCompIso F P
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_nat : ∀ (n : ℕ), Cardinal.toENat ↑n = ↑n
-- Mathlib.Algebra.GroupWithZero.Action.Hom
ZeroHom.smul_apply : ∀ {M : Type u_1} {A : Type u_3} {B : Type u_4} [inst : Zero A] [inst_1 : Zero B] [inst_2 : SMulZeroClass M B] (m : M)
  (f : ZeroHom A B) (a : A), (m • f) a = m • f a
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffOn.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {H'' : Type u_6} [inst_7 : TopologicalSpace H''] {E'' : Type u_7}
  [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E''] {I'' : ModelWithCorners 𝕜 E'' H''} {G : Type u_8}
  [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H G] {M : Type u_9} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace H'' N]
  [inst_16 : SMul G M] {n : WithTop ℕ∞} [ContMDiffSMul I I' n G M] {f : N → G} {g : N → M} {s : Set N},
  ContMDiffOn I'' I n f s → ContMDiffOn I'' I' n g s → ContMDiffOn I'' I' n (f • g) s
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.comap_primeIdealOf_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {x : ↥X} (U : Y.Opens) (hU : AlgebraicGeometry.IsAffineOpen U)
  (V : X.Opens) (hV : AlgebraicGeometry.IsAffineOpen V) (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U)
  (hx : x ∈ V),
  PrimeSpectrum.comap (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V hVU)) (hV.primeIdealOf ⟨x, hx⟩) =
    hU.primeIdealOf ⟨f x, ⋯⟩
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- A function is `C^(n + 1)` on a domain with unique derivatives if and only if it is
differentiable there, and its derivative (expressed with `fderivWithin`) is `C^n`.  -/
contDiffOn_succ_iff_fderivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞},
  UniqueDiffOn 𝕜 s →
    (ContDiffOn 𝕜 (n + 1) f s ↔
      DifferentiableOn 𝕜 f s ∧ (n = ⊤ → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (fderivWithin 𝕜 f s) s)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.mem_sup_left : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A}
  {x : A}, x ∈ S → x ∈ S ⊔ T
-- Init.Data.String.Lemmas.Iterate
String.Model.positionsFrom_eq_cons : ∀ {s : String} {p : s.Pos} (hp : p ≠ s.endPos),
  String.Model.positionsFrom p = ⟨p, hp⟩ :: String.Model.positionsFrom (p.next hp)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.OuterRegular.smul : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] (μ : MeasureTheory.Measure α) [μ.OuterRegular]
  {x : ENNReal}, x ≠ ⊤ → (x • μ).OuterRegular
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
/-- A smooth Riemannian metric defines in particular a continuous Riemannian metric.  -/
Bundle.ContMDiffRiemannianMetric.toContinuousRiemannianMetric : {EB : Type u_1} →
  [inst : NormedAddCommGroup EB] →
    [inst_1 : NormedSpace ℝ EB] →
      {HB : Type u_2} →
        [inst_2 : TopologicalSpace HB] →
          {IB : ModelWithCorners ℝ EB HB} →
            {n : WithTop ℕ∞} →
              {B : Type u_3} →
                [inst_3 : TopologicalSpace B] →
                  [inst_4 : ChartedSpace HB B] →
                    {F : Type u_4} →
                      [inst_5 : NormedAddCommGroup F] →
                        [inst_6 : NormedSpace ℝ F] →
                          {E : B → Type u_5} →
                            [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)] →
                              [inst_8 : (b : B) → TopologicalSpace (E b)] →
                                [inst_9 : (b : B) → AddCommGroup (E b)] →
                                  [inst_10 : (b : B) → Module ℝ (E b)] →
                                    [inst_11 : FiberBundle F E] →
                                      [inst_12 : VectorBundle ℝ F E] →
                                        Bundle.ContMDiffRiemannianMetric IB n F E →
                                          Bundle.ContinuousRiemannianMetric F E
-- Aesop.Forward.Match.Types
Aesop.Match.mk.sizeOf_spec : ∀ (subst : Aesop.Substitution) (patInstSubsts : Array Aesop.Substitution) (level : Aesop.SlotIndex)
  (forwardDeps conclusionDeps : Array Aesop.PremiseIndex),
  sizeOf
      { subst := subst, patInstSubsts := patInstSubsts, level := level, forwardDeps := forwardDeps,
        conclusionDeps := conclusionDeps } =
    1 + sizeOf subst + sizeOf patInstSubsts + sizeOf level + sizeOf forwardDeps + sizeOf conclusionDeps
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- The trailing coefficient of the power of a function is the power of the trailing coefficient.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_fun_zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℤ} {f : 𝕜 → 𝕜},
  MeromorphicAt f x → meromorphicTrailingCoeffAt (fun z => f z ^ n) x = meromorphicTrailingCoeffAt f x ^ n
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_inv_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.unop =
    (CategoryTheory.MonoidalCategoryStruct.associator (Opposite.unop X) (Opposite.unop Y) (Opposite.unop Z)).hom
-- Mathlib.RingTheory.Localization.AtPrime.Extension
/-- The nonzero prime ideals of `Sₚ` are prime ideals over the maximal ideal of `Rₚ`.
See `Localization.AtPrime.primesOverEquivPrimesOver` for the bijection between the prime ideals
of `Sₚ` over the maximal ideal of `Rₚ` and the primes ideals of `S` above `p`.
 -/
IsLocalization.AtPrime.mem_primesOver_of_isPrime : ∀ (Rₚ : Type u_3) [inst : CommRing Rₚ] [inst_1 : IsLocalRing Rₚ] (Sₚ : Type u_4) [inst_2 : CommRing Sₚ]
  [inst_3 : Algebra Rₚ Sₚ] {Q : Ideal Sₚ} [Q.IsMaximal] [Algebra.IsIntegral Rₚ Sₚ],
  Q ∈ (IsLocalRing.maximalIdeal Rₚ).primesOver Sₚ
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.erase_neg : ∀ {ι : Type u} [inst : DecidableEq ι] {β : ι → Type v} [inst_1 : (i : ι) → AddGroup (β i)] (i : ι)
  (f : Π₀ (i : ι), β i), DFinsupp.erase i (-f) = -DFinsupp.erase i f
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.descColimitType_comp_ι : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w₀)) (c : F.CoconeTypes)
  (j : J), F.descColimitType c ∘ F.ιColimitType j = c.ι j
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.isSymm_toMatrix_iff_isSymm : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  {B : LinearMap.BilinForm R₁ M₁}, ((LinearMap.BilinForm.toMatrix b) B).IsSymm ↔ B.IsSymm
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_map_of_injective : ∀ {R : Type u} {S : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] (p : MvPolynomial σ R)
  {f : R →+* S}, Function.Injective ⇑f → ((MvPolynomial.map f) p).degrees = p.degrees
-- Mathlib.Topology.Order.LeftRight
Filter.Eventually.exists_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] {a : α} [(nhdsWithin a (Set.Iio a)).NeBot]
  {p : α → Prop}, (∀ᶠ (x : α) in nhds a, p x) → ∃ b < a, p b
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTransposeAddEquiv_symm : ∀ (m : Type u_2) (n : Type u_3) (α : Type v) [inst : AddMonoid α] [inst_1 : StarAddMonoid α],
  (Matrix.conjTransposeAddEquiv m n α).symm = Matrix.conjTransposeAddEquiv n m α
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_iff_enorm : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤
-- Mathlib.Algebra.Torsor.Defs
smul_sdiv_smul_cancel_right : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (v₁ v₂ : G) (p : P), v₁ • p /ₛ v₂ • p = v₁ / v₂
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
HasFDerivAt.lim_real : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {f' : E →L[ℝ] F} {x : E},
  HasFDerivAt f f' x → ∀ (v : E), Filter.Tendsto (fun c => c • (f (x + c⁻¹ • v) - f x)) Filter.atTop (nhds (f' v))
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.eq_of_heq : ∀ {α : Sort u} {a a' : α}, a ≍ a' → a = a'
-- Init.Sym.Lemmas
Lean.Sym.UInt16.lt_eq_false : ∀ (a b : UInt16), decide (a < b) = false → (a < b) = False
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearRupUnits.eq_1 : ∀ {n : ℕ} (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }.clearRupUnits =
    { clauses := clauses, rupUnits := #[], ratUnits := ratUnits,
      assignments := Array.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit assignments rupUnits }
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Limits.compCoyonedaSectionsEquiv_symm_apply_coe : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J C) (X : C)
  (τ : (CategoryTheory.Functor.const J).obj X ⟶ F) (X_1 : J),
  ↑((CategoryTheory.Limits.compCoyonedaSectionsEquiv F X).symm τ) X_1 = τ.app X_1
-- Std.Http.Data.Version
/-- Converts a `Version` to its corresponding major and minor numbers as a pair.
 -/
Std.Http.Version.toNumber : Std.Http.Version → ℕ × ℕ
-- Mathlib.Topology.Sets.Compacts
/-- The compact neighbourhood induced by the existence of an open subset between two compacts  -/
TopologicalSpace.Compacts.compactNhdsMkOfOpens : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    {K : TopologicalSpace.Compacts α} →
      (L : TopologicalSpace.Compacts α) → (U : TopologicalSpace.Opens α) → ↑K ⊆ ↑U → ↑U ⊆ ↑L → ↑K.compactNhds
-- Mathlib.Analysis.Calculus.Deriv.Prod
derivWithin_pi : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_1} {E' : ι → Type u_2}
  [inst_1 : (i : ι) → NormedAddCommGroup (E' i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E' i)] {φ : 𝕜 → (i : ι) → E' i},
  (∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => φ x i) s x) →
    derivWithin φ s x = fun i => derivWithin (fun x => φ x i) s x
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeFintypeCatSingleObjInclOfFinite : ∀ {G : Type v} [inst : Group G] [Finite G],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.SingleObj G) FintypeCat.incl
-- Std.Time.Date.Unit.Week
Std.Time.Week.Aligned.instOrdOrdinal : Ord Std.Time.Week.Aligned.Ordinal
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (fg' : i' ⟶ k')
  (h' : CategoryTheory.CategoryStruct.comp f' g' = fg')
  (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g')
  (β : CategoryTheory.ComposableArrows.mk₁ fg ⟶ CategoryTheory.ComposableArrows.mk₁ fg') (n : ℤ),
  autoParam (β.app 0 = α.app 0) CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles._auto_1 →
    autoParam (β.app 1 = α.app 2) CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles._auto_3 →
      CategoryTheory.CategoryStruct.comp (X.opcyclesMap f g f' g' α n) (X.fromOpcycles f' g' fg' h' n) =
        CategoryTheory.CategoryStruct.comp (X.fromOpcycles f g fg h n) ((X.H n).map β)
-- Mathlib.Condensed.Discrete.LocallyConstant
CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete : (Condensed.discrete (Type (u_1 + 1))).Faithful
-- Mathlib.Algebra.Ring.Defs
NonAssocRing.toNonUnitalNonAssocRing : {α : Type u_1} → [self : NonAssocRing α] → NonUnitalNonAssocRing α
-- Lean.Util.Trace
Lean.TraceState : Type
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.isPullback_of_openCover : ∀ {X Y Z W : AlgebraicGeometry.Scheme} (fWX : W ⟶ X) (fWY : W ⟶ Y) (fXZ : X ⟶ Z) (fYZ : Y ⟶ Z) (𝒰 : X.OpenCover),
  (∀ (i : 𝒰.toPreZeroHypercover.1),
      CategoryTheory.IsPullback (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 fWX i)
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i) fWY)
        (CategoryTheory.CategoryStruct.comp (𝒰.f i) fXZ) fYZ) →
    CategoryTheory.IsPullback fWX fWY fXZ fYZ
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Option.getD.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : α) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match some x with
    | some x => h_1 x
    | none => h_2 ()) =
    h_1 x
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Measure.add_right_inj : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ ν₁ ν₂ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ],
  μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.replace.eq_1 : ∀ {α : Type u} [inst : BEq α] (xs : Array α) (a b : α),
  xs.replace a b =
    match xs.finIdxOf? a with
    | none => xs
    | some i => xs.set (↑i) b ⋯
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.ext : ∀ {α : Type u_1} {x y : GenContFract α}, x.h = y.h → x.s = y.s → x = y
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
SpectrumRestricts.of_rightInvOn : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Semifield S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] {a : A} {f : S → R},
  Function.LeftInverse f ⇑(algebraMap R S) → Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a) → SpectrumRestricts a f
-- Mathlib.Order.Minimal
MinimalFor.not_lt : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {Q : ι → Prop} {f : ι → α} {i j : ι},
  MinimalFor Q f i → Q j → ¬f j < f i
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Turn minimal axioms for `CompleteDistribLattice` into minimal axioms for `Order.Coframe`.  -/
CompleteDistribLattice.MinimalAxioms.toCoframe : ∀ {α : Type u} [inst : CompleteLattice α], CompleteDistribLattice.MinimalAxioms α → Order.Coframe.MinimalAxioms α
-- Mathlib.Data.Multiset.Defs
Multiset.coe_card : ∀ {α : Type u_1} (l : List α), (↑l).card = l.length
-- Mathlib.Topology.UniformSpace.UniformEmbedding
Dense.extend_spec : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {s : Set α} {f : ↑s → β}
  [CompleteSpace β] (hs : Dense s),
  UniformContinuous f → ∀ (a : α), Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds (hs.extend f a))
-- Mathlib.Data.Array.Defs
/-- Permute the array using a list of cycles.  -/
Array.permute! : {α : Type u} → [Inhabited α] → Array α → List (List ℕ) → Array α
-- Init.Data.List.Lemmas
List.flatMap_eq_nil_iff : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β}, List.flatMap f l = [] ↔ ∀ x ∈ l, f x = []
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
/-- If `e : c.Embedding c'` is an embedding of complex shapes,
`f` and `g` are morphism between cochain complexes of shape `c`,
this is the bijection between homotopies between `f` and `g`,
and homotopies between the extensions `extendMap f e` and `extendMap g e`.  -/
Homotopy.extendEquiv : {ι : 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.Preadditive C] →
                {K L : HomologicalComplex C c} →
                  {f g : K ⟶ L} →
                    (e : c.Embedding c') →
                      [e.IsRelIff] →
                        Homotopy f g ≃ Homotopy (HomologicalComplex.extendMap f e) (HomologicalComplex.extendMap g e)
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.join_nil : ∀ {α : Type u} (a : α) (S : Stream'.Seq (Stream'.Seq1 α)), Stream'.Seq1.join ((a, Stream'.Seq.nil), S) = (a, S.join)
-- Init.Data.Fin.Lemmas
Fin.modn_val : ∀ {n : ℕ} (a : Fin n) (b : ℕ), ↑(a.modn b) = ↑a % b
-- Mathlib.Logic.Equiv.Fin.Basic
/-- `Equiv` between `Fin (n + 1)` and `Option (Fin n)` sending `Fin.last n` to `none`  -/
finSuccEquivLast : {n : ℕ} → Fin (n + 1) ≃ Option (Fin n)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the reverse direction of `Equiv.Perm.isCycleOn_inv`. -/
Equiv.Perm.IsCycleOn.inv : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α}, f.IsCycleOn s → f⁻¹.IsCycleOn s
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.spanningSets_mono : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SigmaFinite μ] {m n : ℕ},
  m ≤ n → MeasureTheory.spanningSets μ m ⊆ MeasureTheory.spanningSets μ n
-- Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
HasStrictFDerivAt.eventually_apply_eq_iff_implicitFunctionOfProdDomain : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂]
  [inst_5 : NormedSpace 𝕜 E₂] [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {f'u : E₁ × E₂ →L[𝕜] F}
  (dfu : HasStrictFDerivAt f f'u u) (if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  ∀ᶠ (v : E₁ × E₂) in nhds u, f v = f u ↔ dfu.implicitFunctionOfProdDomain if₂u v.1 = v.2
-- Mathlib.GroupTheory.OrderOfElement
/-- **Alias** of the reverse direction of `isOfFinOrder_inv_iff`.

---

Inverses of elements of finite order have finite order.  -/
IsOfFinOrder.inv : ∀ {G : Type u_1} [inst : Group G] {x : G}, IsOfFinOrder x → IsOfFinOrder x⁻¹
-- Init.Data.Nat.Lemmas
Nat.mod_div_self : ∀ (m n : ℕ), m % n / n = 0
-- Mathlib.CategoryTheory.Sites.Closed
/-- The sieve `S` is closed iff its closure is equal to itself.  -/
CategoryTheory.GrothendieckTopology.isClosed_iff_close_eq_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
  (S : CategoryTheory.Sieve X), J₁.IsClosed S ↔ J₁.close S = S
-- Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
/-- Kaplansky's criterion: an integral domain is a UFD if and only if every nonzero prime ideal
contains a prime element.  -/
UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime : ∀ {R : Type u_1} [inst : CommSemiring R] [IsDomain R],
  UniqueFactorizationMonoid R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.hasTacticAlt : Lean.Syntax → Bool
-- Mathlib.Data.Rat.Floor
Rat.cast_fract : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : ℚ),
  ↑(Int.fract x) = Int.fract ↑x
-- Batteries.Data.List.Perm
List.Perm.union_right : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α] (t₁ : List α), l₁.Perm l₂ → (l₁ ∪ t₁).Perm (l₂ ∪ t₁)
-- Mathlib.Analysis.RCLike.Sqrt
RCLike.sqrt_eq_ite : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {a : 𝕜},
  RCLike.sqrt a =
    if h : RCLike.im RCLike.I = 1 then (RCLike.complexRingEquiv h).symm ((RCLike.complexRingEquiv h) a).sqrt
    else ↑√(RCLike.re a)
-- Mathlib.AlgebraicTopology.CechNerve
/-- The Čech nerve associated to an arrow.  -/
CategoryTheory.Arrow.cechNerve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (f : CategoryTheory.Arrow C) →
      [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] →
        CategoryTheory.SimplicialObject C
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
CategoryTheory.Functor.IsWellOrderContinuous.restriction_setIci : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J]
  {F : CategoryTheory.Functor J C} [F.IsWellOrderContinuous] (j : J), (⋯.functor.comp F).IsWellOrderContinuous
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- If `X ⟶ Y` is an open immersion, and `Y` is a SheafedSpace, then so is `X`.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : AlgebraicGeometry.PresheafedSpace C} →
      (Y : AlgebraicGeometry.SheafedSpace C) →
        (f : X ⟶ Y.toPresheafedSpace) →
          [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] → AlgebraicGeometry.SheafedSpace C
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- **Alias** of `smul_apply`. -/
ContinuousMultilinearMap.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.comp_continuousOn_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {γ : Type u_3}
  [inst_2 : TopologicalSpace γ], Isometry f → ∀ {g : γ → α} {s : Set γ}, ContinuousOn (f ∘ g) s ↔ ContinuousOn g s