mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.logMap_unit_smul : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K}
  (u : (NumberField.RingOfIntegers K)ˣ),
  NumberField.mixedEmbedding.norm x ≠ 0 →
    NumberField.mixedEmbedding.logMap (u • x) =
      (NumberField.Units.logEmbedding K) (Additive.ofMul u) + NumberField.mixedEmbedding.logMap x
-- Mathlib.RingTheory.Lasker
Submodule.IsMinimalPrimaryDecomposition.injOn : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (N : Submodule R M) (t : Finset (Submodule R M)),
  N.IsMinimalPrimaryDecomposition t → Set.InjOn (fun J => (J.colon Set.univ).radical) ↑t
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Methods.mk.sizeOf_spec : ∀ (pre post : Lean.Meta.Sym.DSimp.DSimproc), sizeOf { pre := pre, post := post } = 1
-- Lean.Message
Lean.NamingContext.mk.inj : ∀ {currNamespace : Lean.Name} {openDecls : List Lean.OpenDecl} {currNamespace_1 : Lean.Name}
  {openDecls_1 : List Lean.OpenDecl},
  { currNamespace := currNamespace, openDecls := openDecls } =
      { currNamespace := currNamespace_1, openDecls := openDecls_1 } →
    currNamespace = currNamespace_1 ∧ openDecls = openDecls_1
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.Equivalence_mk'_unitInv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C)
  (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse)
  (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D)
  (f :
    ∀ (X : C),
      CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) =
        CategoryTheory.CategoryStruct.id (functor.obj X)),
  { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso,
        functor_unitIso_comp := f }.unitInv =
    unit_iso.inv
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolRing_toBoolRing : ∀ {α : Type u_1} (a : α), ofBoolRing (toBoolRing a) = a
-- Lean.Data.Json.Basic
Lean.JsonNumber.mk : ℤ → ℕ → Lean.JsonNumber
-- Mathlib.Algebra.Order.Floor.Defs
Int.gc_ceil_coe : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α], GaloisConnection Int.ceil Int.cast
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and `+` is an additive left cancel monoid, if it
admits an injective map that preserves `0` and `+` to an additive left cancel monoid.  -/
Function.Injective.addLeftCancelMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : SMul ℕ M₁] →
          [inst_3 : AddLeftCancelMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 0 = 0 →
                  (∀ (x y : M₁), f (x + y) = f x + f y) →
                    (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) → AddLeftCancelMonoid M₁
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
CategoryTheory.SmallObject.SuccStruct.instIsWellOrderContinuousIterationFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C], (Φ.iterationFunctor J).IsWellOrderContinuous
-- Mathlib.RingTheory.Polynomial.Wronskian
Polynomial.wronskian.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (a b : Polynomial R),
  a.wronskian b = a * Polynomial.derivative b - Polynomial.derivative a * b
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
CategoryTheory.instIsCardinalAccessibleCategoryOfIsCardinalLocallyPresentable : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalLocallyPresentable C κ], CategoryTheory.IsCardinalAccessibleCategory C κ
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.ofSpan_apply_self : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  (hs : ⊤ ≤ Submodule.span K s) (x : ↑(⋯.extend ⋯)), (Module.Basis.ofSpan hs) x = ↑x
-- Init.Data.Float.Model.Unpacked.Pack.Basic
/-- Unpacks the sign bit of the packed float.
 -/
Float.Model.UnpackedFloat.unpackSign : {spec : Float.Model.Format} → BitVec spec.numBits → BitVec 1
-- Mathlib.Order.Monotone.Defs
monotone_prodMk_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : γ → α}
  {g : γ → β}, (Monotone fun x => (f x, g x)) ↔ Monotone f ∧ Monotone g
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_apply : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x₀ : M} {V W : (x : M) → TangentSpace I x},
  VectorField.mlieBracketWithin I V W s x₀ =
    (mfderiv% ↑(extChartAt I x₀) x₀).inverse
      (VectorField.lieBracketWithin 𝕜
        (VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) V (Set.range ↑I))
        (VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) W (Set.range ↑I))
        (↑(extChartAt I x₀).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x₀) x₀))
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Generalised ultrametric triangle inequality for nonempty finite products in commutative groups with
an ultrametric norm.
 -/
IsUltrametricDist.norm_prod_le_of_forall_le_of_nonempty : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] {s : Finset ι},
  s.Nonempty → ∀ {f : ι → M} {C : ℝ}, (∀ i ∈ s, ‖f i‖ ≤ C) → ‖∏ i ∈ s, f i‖ ≤ C
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.sSup_eq : ∀ {α : Type u_1} [inst : LE α] [inst_1 : SupSet α] {s : Set (WithTop α)},
  ⊤ ∉ s → BddAbove (WithTop.some ⁻¹' s) → sSup s = ↑(sSup (WithTop.some ⁻¹' s))
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldlM_eq_foldlM_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {a : Type u_1} {f : a → α → m a} {init : a} [inst : Monad m] [LawfulMonad m]
  {t : RBTree.RBNode α}, RBTree.RBNode.foldlM f init t = List.foldlM f init t.toList
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.isEmbedding : ∀ {α : Type u_4} {β : Type u_5} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → Continuous f → Topology.IsEmbedding f
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
/-- A nonnegative nonarchimedean function satisfies the triangle inequality.  -/
IsNonarchimedean.add_le : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {α : Type u_2} [inst_3 : Add α]
  {f : α → R}, (∀ (x : α), 0 ≤ f x) → IsNonarchimedean f → ∀ {a b : α}, f (a + b) ≤ f a + f b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.filterMap_equiv_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {f : α → β → Bool},
  t.WF → (Std.TreeMap.Raw.filterMap (fun k => Option.guard fun v => f k v) t).Equiv (Std.TreeMap.Raw.filter f t)
-- Mathlib.Data.Nat.ModEq
Nat.modEq_zero_iff_dvd : ∀ {n a : ℕ}, a ≡ 0 [MOD n] ↔ n ∣ a
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.Hom2.op2'.sizeOf_spec : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : Bᵒᵖ} {f g : a ⟶ b} [inst_1 : SizeOf B]
  (unop2 : f.unop ⟶ g.unop), sizeOf { unop2 := unop2 } = 1 + sizeOf unop2
-- Lean.Data.PPContext
Lean.PPContext.opts : Lean.PPContext → Lean.Options
-- Mathlib.CategoryTheory.Shift.Localization
/-- The localized category `W.Localization'` is endowed with the induced shift.  -/
CategoryTheory.HasShift.localization' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (A : Type w) →
        [inst_1 : AddMonoid A] →
          [inst_2 : CategoryTheory.HasShift C A] →
            [W.IsCompatibleWithShift A] → [inst_4 : W.HasLocalization] → CategoryTheory.HasShift W.Localization' A
-- Init.Sym.Lemmas
Lean.Sym.Rat.le_eq_false : ∀ (a b : ℚ), decide (a ≤ b) = false → (a ≤ b) = False
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roo.count_iter : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] [inst_6 : Std.Rxo.HasSize α] [Std.Rxo.LawfulHasSize α] {r : Std.Roo α},
  r.iter.length = r.size
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- The function `(f, x) ↦ update f a x : (Π a, X a) × X a → Π a, X a` is measurable.  -/
measurable_update' : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] {a : δ} [inst_1 : DecidableEq δ],
  Measurable fun p => Function.update p.1 a p.2
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.of_comp_eq_base : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Monoid (G i)] [inst_1 : Monoid H]
  {φ : (i : ι) → H →* G i} (i : ι), (Monoid.PushoutI.of i).comp (φ i) = Monoid.PushoutI.base φ
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balLeft.match_4.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (l : RBTree.RBNode α) →
      ((a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a x b)) →
        ((l : RBTree.RBNode α) →
            (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
                l = RBTree.RBNode.node RBTree.RBColor.red a x b → False) →
              motive l) →
          motive l
-- Aesop.Rule.Name
_private.Aesop.Rule.Name.0.Aesop.RuleName.Json.scope : Aesop.RuleName.Json✝ → Aesop.ScopeName
-- Mathlib.Control.Functor
/-- Extract the element of `α` from the constant functor.  -/
Functor.AddConst.run : {α : Type u_1} → {β : Type u_2} → Functor.AddConst α β → α
-- Mathlib.Topology.Closure
IsOpen.interior_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → interior s = s
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- Some glue, verifying that the structure presheaf valued in `CommRing` agrees with the
`Type`-valued structure presheaf.  -/
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafCompForget : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              CategoryTheory.Functor.comp
                  (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing 𝒜)
                  (CategoryTheory.forget CommRingCat) ≅
                (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType 𝒜).obj
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instRing : {R : Type u_1} → [inst : TopologicalSpace R] → [inst_1 : Ring R] → [IsTopologicalRing R] → Ring (SeparationQuotient R)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneRightOpOfCoconeEquiv_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C},
  CategoryTheory.Limits.coneRightOpOfCoconeEquiv.unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)ᵒᵖ)
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_nsmul : ∀ (K : Type u_1) {E : Type u_2} [inst : RCLike K] [inst_1 : NormedAddCommGroup E] [NormedSpace K E] (n : ℕ) (x : E),
  ‖n • x‖ = n • ‖x‖
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.MkSimpContextResult.mk : Lean.Meta.Simp.Context →
  Lean.Meta.Simp.SimprocsArray →
    Lean.Elab.Tactic.Simp.DischargeWrapper →
      Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult) → Lean.Elab.Tactic.MkSimpContextResult
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Scalar multiples of harmonic functions are harmonic.
 -/
InnerProductSpace.HarmonicOnNhd.const_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E} {c : ℝ},
  InnerProductSpace.HarmonicOnNhd f s → InnerProductSpace.HarmonicOnNhd (c • f) s
-- Mathlib.Analysis.Distribution.TestFunction
/-- Given `T : F →L[𝕜] F'`, `postcompCLM T` is the continuous `𝕜`-linear-map sending
`f : 𝓓^{n}(Ω, F)` to `T ∘ f` as an element of `𝓓^{n}(Ω, F')`.  -/
TestFunction.postcompCLM : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace ℝ E] →
          {Ω : TopologicalSpace.Opens E} →
            {F : Type u_4} →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace ℝ F] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    {F' : Type u_5} →
                      [inst_6 : NormedAddCommGroup F'] →
                        [inst_7 : NormedSpace ℝ F'] →
                          [inst_8 : NormedSpace 𝕜 F'] →
                            {n : ℕ∞} →
                              [inst_9 : Algebra ℝ 𝕜] →
                                [inst_10 : IsScalarTower ℝ 𝕜 F] →
                                  [inst_11 : IsScalarTower ℝ 𝕜 F'] →
                                    (F →L[𝕜] F') → TestFunction Ω F n →L[𝕜] TestFunction Ω F' n
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- the induced map on right homology  -/
CategoryTheory.ShortComplex.RightHomologyMapData.φH : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.RightHomologyData} →
            {h₂ : S₂.RightHomologyData} → CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂ → (h₁.H ⟶ h₂.H)
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
/-- A matrix `M` is right-separating if for all `w ≠ 0`, there is a `v` with `v * M * w ≠ 0`.  -/
Matrix.SeparatingRight : {m : Type u_1} →
  {n : Type u_2} → {R : Type u_3} → [NonUnitalNonAssocSemiring R] → [Finite m] → [Finite n] → Matrix m n R → Prop
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_eq_singleton_append_iff : ∀ {xs : Array ℕ} {m n a : ℕ}, (m<...n).toArray = #[a] ++ xs ↔ m + 1 = a ∧ m + 1 < n ∧ ((m + 1)<...n).toArray = xs
-- Mathlib.Order.Cover
WCovBy.inf_eq : ∀ {α : Type u_1} [inst : SemilatticeInf α] {a b c : α}, c ⩿ a → c ⩿ b → a ≠ b → a ⊓ b = c
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wf_insertManyIfNew₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w}
  [inst_4 : ForIn Id ρ ((a : α) × β a)] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size} {l : ρ},
  m.WF → (↑↑(Std.DHashMap.Internal.Raw₀.insertManyIfNew ⟨m, h⟩ l)).WF
-- Mathlib.Algebra.Group.Torsion
zsmul_right_injective : ∀ {G : Type u_2} [inst : AddGroup G] [IsAddTorsionFree G] {n : ℤ}, n ≠ 0 → Function.Injective fun a => n • a
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- If 'f' is *not* circle integrable, then the circle average is zero by definition.
 -/
Real.circleAverage.integral_undef : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ},
  ¬CircleIntegrable f c R → Real.circleAverage f c R = 0
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RooSliceData.mk.injEq : ∀ {α : Type u} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit) (range : Std.Roo α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit) (range_1 : Std.Roo α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for `𝟙 a`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₁.id₁M : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
    Mathlib.Tactic.BicategoryLike.Obj → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Probability.Density
MeasureTheory.measurable_pdf : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} (X : Ω → E)
  (ℙ : MeasureTheory.Measure Ω) (μ : autoParam (MeasureTheory.Measure E) MeasureTheory.measurable_pdf._auto_1),
  Measurable (MeasureTheory.pdf X ℙ μ)
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.bot : ∀ (S : Type u_5) [inst : Semiring S] (M : Type u_6) [inst_1 : AddCommMonoid M] [inst_2 : Module S M],
  LinearMap.IsProj ⊥ 0
-- Mathlib.Topology.Order.OrderClosed
Dense.exists_between : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] [DenselyOrdered α]
  {s : Set α}, Dense s → ∀ {x y : α}, x < y → ∃ z ∈ s, z ∈ Set.Ioo x y
-- Mathlib.Order.Minimal
minimal_mem_image_monotone_iff : ∀ {α : Type u_2} {β : Type u_3} {a : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  a ∈ s →
    (∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) →
      (Minimal (fun x => x ∈ f '' s) (f a) ↔ Minimal (fun x => x ∈ s) a)
-- Mathlib.GroupTheory.IsSubnormal
/-- A subgroup `H` is subnormal if there is a subnormal subgroup `K` containing `H` that is
subnormal itself and such that `H` is normal in `K`.  -/
Subgroup.IsSubnormal.step : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), H ≤ K → K.IsSubnormal → (H.subgroupOf K).Normal → H.IsSubnormal
-- Mathlib.MeasureTheory.Order.Group.Lattice
measurable_leOnePart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [inst_2 : MeasurableSpace α] [MeasurableInv α] [MeasurableSup α],
  Measurable leOnePart
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Cell.alter.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α] {k : α}
  (f : Option (β k) → Option (β k)) (c : Std.DTreeMap.Internal.Cell α β (compare k)),
  Std.DTreeMap.Internal.Cell.alter f c =
    match h : c.inner with
    | none => Std.DTreeMap.Internal.Cell.ofOption k (f none)
    | some ⟨k', v'⟩ =>
      have heq := ⋯;
      Std.DTreeMap.Internal.Cell.ofOption k (f (some (cast heq v')))
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.jacobianOfHasCoeffs.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P P_1 : Algebra.SubmersivePresentation R S ι σ) (e_P : P = P_1)
  (R₀ : Type u_5) [inst_4 : CommRing R₀] [inst_5 : Algebra R₀ R] [inst_6 : Algebra R₀ S] [inst_7 : IsScalarTower R₀ R S]
  [inst_8 : P.HasCoeffs R₀], P.jacobianOfHasCoeffs R₀ = P_1.jacobianOfHasCoeffs R₀
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapAlgHom_id : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M], AddMonoidAlgebra.mapAlgHom M (AlgHom.id R A) = AlgHom.id R (AddMonoidAlgebra A M)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.exists_adj_isEdgeReachable_two : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V},
  u ≠ v → G.IsEdgeReachable 2 u v → ∃ w, G.Adj u w ∧ G.IsEdgeReachable 2 u w
-- Mathlib.CategoryTheory.MorphismProperty.Quotient
CategoryTheory.MorphismProperty.eq_inverseImage_quotientFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  (homRel : HomRel C) [inst_1 : CategoryTheory.HomRel.IsStableUnderPrecomp homRel]
  [inst_2 : CategoryTheory.HomRel.IsStableUnderPostcomp homRel] [inst_3 : W.HasQuotient homRel],
  W = (W.quotient homRel).inverseImage (CategoryTheory.Quotient.functor homRel)
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_lt_self_iff : ∀ {x : ℝ}, √x < x ↔ 1 < x
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Embedding.subtype_comp_codRestrict : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N) (p : L.Substructure N) (h : ∀ (b : M), f b ∈ p),
  p.subtype.comp (FirstOrder.Language.Embedding.codRestrict p f h) = f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z}, CategoryTheory.IsPushout g.op f.op snd.op fst.op ↔ CategoryTheory.IsPullback fst snd f g
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_singleton : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {k : α},
  ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity [k]) =
    Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertIfNew k ()
-- Mathlib.LinearAlgebra.SymplecticGroup
Matrix.symplecticGroup.eq_1 : ∀ (l : Type u_1) (R : Type u_2) [inst : DecidableEq l] [inst_1 : CommRing R] [inst_2 : Fintype l],
  Matrix.symplecticGroup l R =
    { carrier := {A | A * Matrix.J l R * A.transpose = Matrix.J l R}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Topology.Order.IntermediateValue
isPreconnected_Ico : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α}, IsPreconnected (Set.Ico a b)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The morphism to `K.cycles i` that is induced by a "cycle", i.e. a morphism
to `K.X i` whose postcomposition with the differential is zero.  -/
HomologicalComplex.liftCycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            {i : ι} →
              [inst_2 : K.HasHomology i] →
                {A : C} →
                  (k : A ⟶ K.X i) →
                    (j : ι) → c.next i = j → CategoryTheory.CategoryStruct.comp k (K.d i j) = 0 → (A ⟶ K.cycles i)
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.IsPoly.poly : ∀ {p : ℕ} {f : ⦃R : Type u_2⦄ → [CommRing R] → WittVector p R → WittVector p R} [self : WittVector.IsPoly p f],
  ∃ φ,
    ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : WittVector p R), (f x).coeff = fun n => (MvPolynomial.aeval x.coeff) (φ n)
-- Mathlib.Topology.MetricSpace.Cover
Metric.isCover_empty_right : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} {s : Set X}, Metric.IsCover ε s ∅ ↔ s = ∅
-- Init.Data.SInt.Lemmas
Int16.add_eq_left : ∀ {a b : Int16}, a + b = a ↔ b = 0
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedOrderHom α β) (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.getD_leftInvSeq_mul_self : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ),
  (cs.leftInvSeq ω).getD j 1 * (cs.leftInvSeq ω).getD j 1 = 1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- The quotient of `V` by the `SimpleGraph.Reachable` relation gives the connected
components of a graph.  -/
SimpleGraph.ConnectedComponent : {V : Type u} → SimpleGraph V → Type u
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.Mono.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y},
  (∀ {Z : C} (g h : Z ⟶ X), CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp h f → g = h) →
    CategoryTheory.Mono f
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.coe_mker : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F), ↑(MonoidHom.mker f) = ⇑f ⁻¹' {1}