mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Preorder.Finite
Finset.exists_maximalFor : ∀ {ι : Type u_1} {α : Type u_2} [inst : LE α] [IsTrans α LE.le] (f : ι → α) (s : Finset ι),
  s.Nonempty → ∃ i, MaximalFor (fun x => x ∈ s) f i
-- Mathlib.Topology.Connected.PathConnected
Prod.instPathConnectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [PathConnectedSpace X]
  [PathConnectedSpace Y], PathConnectedSpace (X × Y)
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.exp_neg_llr' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  ν.AbsolutelyContinuous μ → (fun x => Real.exp (-MeasureTheory.llr μ ν x)) =ᵐ[ν] fun x => (ν.rnDeriv μ x).toReal
-- Aesop.Tree.Data
Aesop.instInhabitedGoalState.default : Aesop.GoalState
-- Mathlib.Algebra.Polynomial.DenomsClearable
denomsClearable_zero : ∀ {R : Type u_1} {K : Type u_2} [inst : Semiring R] [inst_1 : CommSemiring K] {i : R →+* K} {b : R} {bi : K} (N : ℕ)
  (a : R), bi * i b = 1 → DenomsClearable a b N 0 i
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context.inBottomUp : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context → Bool
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.smul_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_3 : Semiring R] [inst_4 : CategoryTheory.Linear R C]
  [inst_5 : ∀ (n : ℤ), CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor C n)] (n : R) (f : T₁ ⟶ T₂),
  (n • f).hom₁ = n • f.hom₁
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.foldlM.match_1.eq_2 : ∀ {m : Type u_3 → Type u_4} {s : Type u_3} {α : Type u_1} (motive : (s → α → m s) → s → List α → Sort u_2)
  (f : s → α → m s) (s_1 : s) (a : α) (as : List α) (h_1 : (x : s → α → m s) → (s : s) → motive x s [])
  (h_2 : (f : s → α → m s) → (s : s) → (a : α) → (as : List α) → motive f s (a :: as)),
  (match f, s_1, a :: as with
    | x, s, [] => h_1 x s
    | f, s, a :: as => h_2 f s a as) =
    h_2 f s_1 a as
-- Mathlib.NumberTheory.LSeries.Dirichlet
ArithmeticFunction.convolution_vonMangoldt_const_one : LSeries.convolution (fun n => ↑(ArithmeticFunction.vonMangoldt n)) 1 = fun n => Complex.log ↑n
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.toBumpCovering.congr_simp : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs fs_1 : SmoothBumpCovering ι I M s),
  fs = fs_1 → ∀ [inst_6 : T2Space M] [inst_7 : IsManifold I (↑⊤) M], fs.toBumpCovering = fs_1.toBumpCovering
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.cg_def : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : L.Substructure M},
  N.CG ↔ ∃ S, S.Countable ∧ (FirstOrder.Language.Substructure.closure L).toFun S = N
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.restrictScalars_neg : ∀ {R : Type u_14} {S : Type u_15} [inst : Semiring R] [inst_1 : Semiring S] {M : Type u_19} {N : Type u_20}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module S M]
  [inst_7 : Module S N] [inst_8 : LinearMap.CompatibleSMul M N R S] (f : M →ₗ[S] N), ↑R (-f) = -↑R f
-- Mathlib.Algebra.Group.End
AddAut.neg_symm : ∀ (M : Type u_2) [inst : Add M] (e : AddAut M), AddEquiv.symm (-e) = e
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_toList_iff_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (k, v) ∈ Std.DTreeMap.Raw.Const.toList t ↔ Std.DTreeMap.Raw.Const.get? t k = some v
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdx?.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → ℕ → Sort u_3) (size : ℕ) (k : α)
  (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (n : ℕ) (h_1 : (x : ℕ) → motive Std.DTreeMap.Internal.Impl.leaf x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) → (n : ℕ) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n),
  (match Std.DTreeMap.Internal.Impl.inner size k v l r, n with
    | Std.DTreeMap.Internal.Impl.leaf, x => h_1 x
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n => h_2 size k v l r n) =
    h_2 size k v l r n
-- Init.Data.BitVec.Lemmas
BitVec.getMsb.eq_1 : ∀ {w : ℕ} (x : BitVec w) (i : Fin w), x.getMsb i = x.getLsb ⟨w - 1 - ↑i, ⋯⟩
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.congr : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f g : X → ε} {μ : MeasureTheory.Measure X} {s : Set X},
  f =ᵐ[μ.restrict s] g → MeasureTheory.LocallyIntegrableOn f s μ → MeasureTheory.LocallyIntegrableOn g s μ
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)),
  (F.mapId b).hom.toNatTrans.app ((F.map f).toFunctor.obj X) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).inv.toNatTrans.app X)
      ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X)
-- Init.Data.Range.Polymorphic.PRange
/-- The intersection operator.  -/
Std.Rio.HasRcoIntersection.intersection : {α : Type w} → [self : Std.Rio.HasRcoIntersection α] → Std.Rio α → Std.Rco α → Std.Rco α
-- Mathlib.Topology.Sheaves.Skyscraper
StalkSkyscraperPresheafAdjunctionAuxs.unit_app : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasColimits C] (x : TopCat.Presheaf C X),
  (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀).app x =
    StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀
      (CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id (TopCat.Presheaf C X)).obj x).stalk p₀))
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.mk_bool : Cardinal.mk Bool = 2
-- Init.GrindInstances.Ring.UInt
UInt32.intCast : IntCast UInt32
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.inhabitedConeMorphism : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (A : CategoryTheory.Limits.Cone F) → Inhabited (CategoryTheory.Limits.ConeMorphism A A)
-- Aesop.Script.SScript
Aesop.Script.SScript.focusAndSolve : ℕ → Aesop.Script.SScript → Aesop.Script.SScript → Aesop.Script.SScript
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_alter!_of_not_compare_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      ¬compare k k' = Ordering.eq →
        Std.DTreeMap.Internal.Impl.contains k' (Std.DTreeMap.Internal.Impl.alter! k f t) =
          Std.DTreeMap.Internal.Impl.contains k' t
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- In a one-dimensional space, any vector is a multiple of any nonzero vector  -/
exists_smul_eq_of_finrank_eq_one : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Module.finrank K V = 1 → ∀ {x : V}, x ≠ 0 → ∀ (y : V), ∃ c, c • x = y
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.upperCentralSeries_eq_center : ∀ (G : Type u_1) [inst : Group G] [Group.IsPerfect G] {n : ℕ},
  n ≠ 0 → Subgroup.upperCentralSeries G n = Subgroup.center G
-- Mathlib.Order.RelClasses
Order.Preimage.instAsymm : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Asymm r] {f : β → α}, Std.Asymm (f ⁻¹'o r)
-- Mathlib.CategoryTheory.Action.Limits
Action.forget_additive : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V], (Action.forget V G).Additive
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_lt_div₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b c d : G₀}, a < c → d ≤ b → 0 ≤ c → 0 < d → a / b < c / d
-- Mathlib.RingTheory.MvPowerSeries.Equiv
_private.Mathlib.RingTheory.MvPowerSeries.Equiv.0.MvPowerSeries.embDomain_finSuccEquiv_cons : ∀ {M : Type u_3} [inst : AddCommMonoid M] {n : ℕ} (i : M) (x : Fin n →₀ M),
  Finsupp.embDomain (finSuccEquiv n).toEmbedding (Finsupp.cons i x) = Finsupp.optionElim i x
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.Lifting.compLeft : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            {E : Type u_3} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
                (F : CategoryTheory.Functor D E) → CategoryTheory.Localization.Lifting L W (L.comp F) F
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f)
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_zero_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), inner 𝕜 x 0 = 0
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.rightUnitor_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Oplax.LaxTrans.rightUnitor η).inv.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
/-- A basic equivalence `A ≌ B'` obtained by composing `eA : A ≌ A'` and `e' : A' ≌ B'`.  -/
AlgebraicTopology.DoldKan.Compatibility.equivalence₀ : {A : Type u_1} →
  {A' : Type u_2} →
    {B' : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} A] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] → (A ≌ A') → (A' ≌ B') → (A ≌ B')
-- Mathlib.Logic.Basic
eq_ite_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {a b c : α}, (a = if P then b else c) ↔ P ∧ a = b ∨ ¬P ∧ a = c
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instMonoid : {M : Type u_1} → [inst : TopologicalSpace M] → [inst_1 : Monoid M] → [ContinuousMul M] → Monoid (SeparationQuotient M)
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderUnitor.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {P : CategoryTheory.MorphismProperty C},
  (∀ (c : C), P (CategoryTheory.MonoidalCategoryStruct.leftUnitor c).hom) →
    (∀ (c : C), P (CategoryTheory.MonoidalCategoryStruct.leftUnitor c).inv) →
      (∀ (c : C), P (CategoryTheory.MonoidalCategoryStruct.rightUnitor c).hom) →
        (∀ (c : C), P (CategoryTheory.MonoidalCategoryStruct.rightUnitor c).inv) → P.IsStableUnderUnitor
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstr.mk : Lean.Grind.CommRing.Poly →
  Bool → Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof → Lean.Meta.Grind.Arith.Linear.RingIneqCnstr
-- Mathlib.RingTheory.DedekindDomain.Basic
/-- A Dedekind domain is an integral domain that is Noetherian, integrally closed, and
has Krull dimension at most one.

This is definition 3.2 of [Neukirch1992].

This is exactly `IsDedekindRing` plus the `IsDomain` hypothesis.

The integral closure condition is independent of the choice of field of fractions:
use `isDedekindDomain_iff` to prove `IsDedekindDomain` for a given `fraction_map`.

This is the default implementation, but there are equivalent definitions,
`IsDedekindDomainDvr` and `IsDedekindDomainInv`.
 -/
IsDedekindDomain : (A : Type u_2) → [CommRing A] → Prop
-- Mathlib.Data.ZMod.Basic
_private.Mathlib.Data.ZMod.Basic.0.ZMod.val.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.swapEquiv_functor_map_hom_toFun : ∀ {X Y : TwoP} (f : X ⟶ Y) (a : X.toBipointed.X),
  (TwoP.swapEquiv.functor.map f).hom.toFun a = (CategoryTheory.ConcreteCategory.hom f.hom) a
-- Mathlib.Data.Set.Pairwise.Basic
/-- **Alias** of `Set.pairwise_insert_of_symm_of_notMem`. -/
Set.pairwise_insert_of_symmetric_of_notMem : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} [Std.Symm r],
  a ∉ s → ((insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_comp : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] {W₂ : Type u_6} {Q₂ : Type u_7}
  [inst_9 : AddCommGroup W₂] [inst_10 : Module R W₂] [inst_11 : TopologicalSpace Q₂] [inst_12 : AddTorsor W₂ Q₂]
  (f : Q →ᴬ[R] Q₂) (g : P →ᴬ[R] Q), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.triangle_mor₃ : ∀ {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.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
  (X.triangle f g).mor₃ = X.δ f g
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- A rotation by the oriented angle `θ`.  -/
Orientation.rotation : {V : Type u_1} →
  [inst : NormedAddCommGroup V] →
    [inst_1 : InnerProductSpace ℝ V] →
      [Fact (Module.finrank ℝ V = 2)] → Orientation ℝ V (Fin 2) → Real.Angle → V ≃ₗᵢ[ℝ] V
-- Mathlib.Topology.NhdsSet
nhdsSet_insert : ∀ {X : Type u_2} [inst : TopologicalSpace X] (x : X) (s : Set X), nhdsSet (insert x s) = nhds x ⊔ nhdsSet s
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearEquiv.mfderivWithin_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E ≃L[𝕜] E') {s : Set E} {x : E}, UniqueMDiffAt[s] x → mfderiv[s] ⇑f x = ↑f
-- Mathlib.Data.Seq.Computation
Computation.get_pure : ∀ {α : Type u} (a : α), (Computation.pure a).get = a
-- Init.Data.String.Lemmas.Order
String.Pos.get_eq_get_ofSlice : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos} {h' : pos ≠ (s.slice p₀ p₁ h).endPos},
  pos.get h' = (String.Pos.ofSlice pos).get ⋯
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCoproducts.isStableUnderCoproductsOfShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C}
  [self : CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{w, v, u} W] (J : Type w),
  W.IsStableUnderCoproductsOfShape J
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasProd_le : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α},
  (∀ (i : ι), f i ≤ g i) → HasProd f a₁ L → HasProd g a₂ L → ∀ [L.NeBot], a₁ ≤ a₂
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.ExtDTreeMap.Const.ofList l cmp).getKey? k = none
-- Mathlib.Order.SupIndep
Finset.SupIndep.image : ∀ {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [inst : Lattice α] [inst_1 : OrderBot α] {f : ι → α}
  [inst_2 : DecidableEq ι] {s : Finset ι'} {g : ι' → ι}, s.SupIndep (f ∘ g) → (Finset.image g s).SupIndep f
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- An alternating map from `ι → M` to `N`, denoted `M [⋀^ι]→ₗ[R] N`,
is a multilinear map that vanishes when two of its arguments are equal.  -/
«term_[⋀^_]→ₗ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Data.Complex.Basic
Complex.div_natCast_re : ∀ (z : ℂ) (n : ℕ), (z / ↑n).re = z.re / ↑n
-- Mathlib.Order.Filter.Partial
Filter.rtendsto'_def : ∀ {α : Type u} {β : Type v} (r : SetRel α β) (l₁ : Filter α) (l₂ : Filter β),
  Filter.RTendsto' r l₁ l₂ ↔ ∀ s ∈ l₂, r.preimage s ∈ l₁
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedCommGroup.toNorm : {E : Type u_8} → [self : SeminormedCommGroup E] → Norm E
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_one : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R), IsLocalization.mk' S x 1 = (algebraMap R S) x
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.min_orderTop_le_orderTop_sub : ∀ {R : Type u_3} [inst : AddGroup R] {Γ : Type u_8} [inst_1 : LinearOrder Γ] {x y : HahnSeries Γ R},
  min x.orderTop y.orderTop ≤ (x - y).orderTop
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- the functor preserves cokernels  -/
CategoryTheory.Functor.PreservesHomology.preservesCokernels : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C}
  {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} {F : CategoryTheory.Functor C D}
  {inst_4 : F.PreservesZeroMorphisms} [self : F.PreservesHomology] ⦃X Y : C⦄ (f : X ⟶ Y),
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F
-- Mathlib.RingTheory.Localization.Away.Basic
Localization.awayLift_mk : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_4} [inst_1 : CommSemiring A] (f : R →+* A) (r a : R) (v : A)
  (hv : f r * v = 1) (j : ℕ), (Localization.awayLift f r ⋯) (Localization.mk a ⟨r ^ j, ⋯⟩) = f a * v ^ j
-- Mathlib.RingTheory.NonUnitalSubring.Basic
RingEquiv.ofLeftInverse'_symm_apply : ∀ {R : Type u} {S : Type v} [inst : NonUnitalRing R] [inst_1 : NonUnitalRing S] {g : S → R} {f : R →ₙ+* S}
  (h : Function.LeftInverse g ⇑f) (x : ↥f.range), (RingEquiv.ofLeftInverse' h).symm x = g ↑x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftRightHomologyComparison_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  S.leftRightHomologyComparison = CategoryTheory.CategoryStruct.comp S.leftHomologyIso.hom S.rightHomologyIso.inv
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instOne.eq_1 : ∀ {α : Type u_1} [inst : One α], OrderDual.instOne = inst
-- Mathlib.Analysis.Analytic.Constructions
/-- The radius of the Cartesian product of two formal series is the minimum of their radii.  -/
FormalMultilinearSeries.radius_prod_eq_min : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (p : FormalMultilinearSeries 𝕜 E F)
  (q : FormalMultilinearSeries 𝕜 E G), (p.prod q).radius = min p.radius q.radius
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_le_of_mem_of_edist_le : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α} {d : ℝ} {x : α},
  x ∈ s → ∀ {y : α}, y ∈ s → x ≠ y → dist x y ≤ d → s.infsep ≤ d
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ1728_c₄ : ∀ (R : Type u_1) [inst : CommRing R], (WeierstrassCurve.ofJ1728 R).c₄ = -48
-- Mathlib.Algebra.Group.Prod
MulHom.coe_prod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N)
  (g : M →ₙ* P), ⇑(f.prod g) = Function.prod ⇑f ⇑g
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
/-- Order-connected component of a point `x` in a set `s`. It is defined as the set of `y` such that
`Set.uIcc x y ⊆ s`. Note that it is empty if and only if `x ∉ s`.  -/
Set.ordConnectedComponent : {α : Type u_1} → [LinearOrder α] → Set α → α → Set α
-- Mathlib.Analysis.Normed.Group.Constructions
pi_norm_const : ∀ {ι : Type u_1} {E : Type u_2} [inst : Fintype ι] [inst_1 : SeminormedAddGroup E] [Nonempty ι] (a : E),
  ‖fun _i => a‖ = ‖a‖
-- Mathlib.Order.Partition.Finpartition
Finpartition.part_eq_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} (P : Finpartition s) {a : α},
  t ∈ P.parts → a ∈ t → P.part a = t
-- Mathlib.Topology.Category.Profinite.Basic
Profinite.toTopCat.reflective : CategoryTheory.Reflective Profinite.toTopCat
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.algebraMap_intNorm_of_isGalois : ∀ (A : Type u_1) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsIntegrallyClosed A] [inst_5 : IsDomain B] [inst_6 : IsIntegrallyClosed B] [inst_7 : Module.Finite A B]
  [inst_8 : Module.IsTorsionFree A B] [IsGalois (FractionRing A) (FractionRing B)] {x : B},
  (algebraMap A B) ((Algebra.intNorm A B) x) = ∏ σ, σ x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.index.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι} {i : ι}
  (c : f.Cell i) [inst_1 : P.IsProper], c.index = c.index
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
/-- If `𝒱` is a refinement of `𝒰` such that `𝒱` is quasicompact, also `𝒰` is quasicompact.  -/
AlgebraicGeometry.QuasiCompactCover.of_hom : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : CategoryTheory.PreZeroHypercover S} {𝒱 : CategoryTheory.PreZeroHypercover S}
  (f : 𝒱.Hom 𝒰) [AlgebraicGeometry.QuasiCompactCover 𝒱], AlgebraicGeometry.QuasiCompactCover 𝒰
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.meromorphicOn_ball_comp_sub_const_iff_meromorphicOn_ball`

---

`MeromorphicOn` is invariant under translation, special case where the set is a ball.  -/
MeromorphicOn.meromorphicOn_ball_fun_comp_sub_const_iff_meromorphicOn_ball : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ},
  MeromorphicOn (fun x => f (x - c)) (Metric.ball c R) ↔ MeromorphicOn f (Metric.ball 0 R)