mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBumpBase.mk.injEq : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (toFun : ℝ → E → ℝ)
  (mem_Icc : ∀ (R : ℝ) (x : E), toFun R x ∈ Set.Icc 0 1) (symmetric : ∀ (R : ℝ) (x : E), toFun R (-x) = toFun R x)
  (smooth : ContDiffOn ℝ (↑⊤) (Function.uncurry toFun) (Set.Ioi 1 ×ˢ Set.univ))
  (eq_one : ∀ (R : ℝ), 1 < R → ∀ (x : E), ‖x‖ ≤ 1 → toFun R x = 1)
  (support : ∀ (R : ℝ), 1 < R → Function.support (toFun R) = Metric.ball 0 R) (toFun_1 : ℝ → E → ℝ)
  (mem_Icc_1 : ∀ (R : ℝ) (x : E), toFun_1 R x ∈ Set.Icc 0 1)
  (symmetric_1 : ∀ (R : ℝ) (x : E), toFun_1 R (-x) = toFun_1 R x)
  (smooth_1 : ContDiffOn ℝ (↑⊤) (Function.uncurry toFun_1) (Set.Ioi 1 ×ˢ Set.univ))
  (eq_one_1 : ∀ (R : ℝ), 1 < R → ∀ (x : E), ‖x‖ ≤ 1 → toFun_1 R x = 1)
  (support_1 : ∀ (R : ℝ), 1 < R → Function.support (toFun_1 R) = Metric.ball 0 R),
  ({ toFun := toFun, mem_Icc := mem_Icc, symmetric := symmetric, smooth := smooth, eq_one := eq_one,
        support := support } =
      { toFun := toFun_1, mem_Icc := mem_Icc_1, symmetric := symmetric_1, smooth := smooth_1, eq_one := eq_one_1,
        support := support_1 }) =
    (toFun = toFun_1)
-- Mathlib.RingTheory.SimpleModule.Basic
Module.Finite.instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule_1 : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : Submodule R M}
  (R₀ : Type u_6) (P : Type u_7) [inst_3 : Semiring R₀] [inst_4 : AddCommMonoid P] [inst_5 : Module R P]
  [inst_6 : Module R₀ M] [inst_7 : SMulCommClass R R₀ M] [inst_8 : SMul R₀ R] [inst_9 : IsScalarTower R₀ R M]
  [Module.Finite R₀ (P →ₗ[R] M)] [IsSemisimpleModule R M], Module.Finite R₀ (P →ₗ[R] ↥m)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I : ∀ {b : ℂ}, 0 < b.re → ∀ (c : ℝ), ∫ (x : ℝ), Complex.exp (-b * (↑x + ↑c * Complex.I) ^ 2) = (↑Real.pi / b) ^ (1 / 2)
-- Init.Data.Nat.Lemmas
Nat.le_sub_iff_add_le' : ∀ {k m n : ℕ}, k ≤ m → (n ≤ m - k ↔ k + n ≤ m)
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.coe_toNat_order : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R}, φ ≠ 0 → ↑φ.order.toNat = φ.order
-- Init.Data.String.Lemmas.FindPos
_private.Init.Data.String.FindPos.0.String.Slice.Pos.prevn.match_1.congr_eq_1 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  n = 0 →
    (match n with
      | 0 => h_1 ()
      | n.succ => h_2 n) ≍
      h_1 ()
-- Mathlib.Algebra.Group.Prod
AddHom.prod.eq_1 : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : M →ₙ+ N)
  (g : M →ₙ+ P), f.prod g = { toFun := Function.prod ⇑f ⇑g, map_add' := ⋯ }
-- Mathlib.Topology.Semicontinuity.Basic
LowerSemicontinuous.inf : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β},
  LowerSemicontinuous f → LowerSemicontinuous g → LowerSemicontinuous fun x => min (f x) (g x)
-- Init.Data.Nat.ToString
Nat.digitChar_eq_a : ∀ {n : ℕ}, n.digitChar = 'a' ↔ n = 10
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- An additive free group basis of an additive free group `G`, over the set `Generators G`.  -/
IsFreeAddGroup.basis : (G : Type u_1) → [inst : AddGroup G] → [inst_1 : IsFreeAddGroup G] → FreeAddGroupBasis (IsFreeAddGroup.Generators G) G
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.EvalConfigItemHandler.mk.inj : ∀ {ref : Lean.Syntax} {key : Lean.Name} {kind : Lean.Elab.ConfigEval.EvalConfigItemHandlerKind} {body : Lean.Term}
  {projFn? struct? : Option Lean.Name} {ref_1 : Lean.Syntax} {key_1 : Lean.Name}
  {kind_1 : Lean.Elab.ConfigEval.EvalConfigItemHandlerKind} {body_1 : Lean.Term}
  {projFn?_1 struct?_1 : Option Lean.Name},
  { ref := ref, key := key, kind := kind, body := body, projFn? := projFn?, struct? := struct? } =
      { ref := ref_1, key := key_1, kind := kind_1, body := body_1, projFn? := projFn?_1, struct? := struct?_1 } →
    ref = ref_1 ∧ key = key_1 ∧ kind = kind_1 ∧ body = body_1 ∧ projFn? = projFn?_1 ∧ struct? = struct?_1
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_congr'_enorm : ∀ {α : Type u_1} {ε : Type u_4} {ε' : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  [inst_1 : ENorm ε'] {f : α → ε} {g : α → ε'},
  (∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) → (MeasureTheory.HasFiniteIntegral f μ ↔ MeasureTheory.HasFiniteIntegral g μ)
-- Mathlib.RingTheory.Localization.Basic
/-- If `S₁` is the localization of `R` at `M₁` and `S₂` is the localization of
`R` at `M₂`, then every localization `T` of `S₂` at `M₁` is also a localization of
`S₁` at `M₂`, in other words `M₁⁻¹M₂⁻¹R` can be identified with `M₂⁻¹M₁⁻¹R`.  -/
IsLocalization.commutes : ∀ {R : Type u_1} [inst : CommSemiring R] (S₁ : Type u_4) (S₂ : Type u_5) (T : Type u_6) [inst_1 : CommSemiring S₁]
  [inst_2 : CommSemiring S₂] [inst_3 : CommSemiring T] [inst_4 : Algebra R S₁] [inst_5 : Algebra R S₂]
  [inst_6 : Algebra R T] [inst_7 : Algebra S₁ T] [inst_8 : Algebra S₂ T] [IsScalarTower R S₁ T] [IsScalarTower R S₂ T]
  (M₁ M₂ : Submonoid R) [IsLocalization M₁ S₁] [IsLocalization M₂ S₂]
  [IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T], IsLocalization (Algebra.algebraMapSubmonoid S₁ M₂) T
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.monic_finprod_of_monic : ∀ {R : Type u} [inst : CommSemiring R] (α : Type u_1) (f : α → Polynomial R),
  (∀ i ∈ Function.mulSupport f, (f i).Monic) → (finprod f).Monic
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.lift_eq_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  (hg : ∀ (y : ↥M), IsUnit (g ↑y)) {x y : R × ↥M},
  (IsLocalization.lift hg) (IsLocalization.mk' S x.1 x.2) = (IsLocalization.lift hg) (IsLocalization.mk' S y.1 y.2) ↔
    g (x.1 * ↑y.2) = g (y.1 * ↑x.2)
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.instHashableDatabase : Hashable Mathlib.CrossRef.Database
-- Lean.Elab.Do.Basic
Lean.Elab.Do.CodeLiveness.noConfusionType : Sort v✝ → Lean.Elab.Do.CodeLiveness → Lean.Elab.Do.CodeLiveness → Sort v✝
-- Mathlib.Algebra.Group.Submonoid.Support
Submonoid.IsMulSpanning.mk : ∀ {G : Type u_1} [inst : Group G] {M : Submonoid G}, (∀ (a : G), a ∈ M ∨ a⁻¹ ∈ M) → M.IsMulSpanning
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
StarAlgEquiv.ofLeftInverse'_apply : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] {g : B → A} {f : F}
  (h : Function.LeftInverse g ⇑f) (x : A), ↑((StarAlgEquiv.ofLeftInverse' h) x) = f x
-- Mathlib.Tactic.Translate.Core
/-- Environment extension used for guessing the translation of a name.  -/
Mathlib.Tactic.Translate.TranslateData.guessNameExt : Mathlib.Tactic.Translate.TranslateData → Mathlib.Tactic.GuessName.GuessNameExt
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.sylvester.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (f g : Polynomial R) (m n : ℕ),
  f.sylvester g m n =
    Matrix.of fun i j =>
      Fin.addCases (fun j₁ => if ↑i ∈ Set.Icc (↑j₁) (↑j₁ + n) then g.coeff (↑i - ↑j₁) else 0)
        (fun j₁ => if ↑i ∈ Set.Icc (↑j₁) (↑j₁ + m) then f.coeff (↑i - ↑j₁) else 0) j
-- Mathlib.Computability.RegularExpressions
RegularExpression.add_rmatch_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (P Q : RegularExpression α) (x : List α),
  (P + Q).rmatch x = true ↔ P.rmatch x = true ∨ Q.rmatch x = true
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.toContinuousMap_compLeft : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  {γ : Type u_5} [inst_3 : TopologicalSpace γ] [inst_4 : Zero γ] {g : C(β, γ)},
  g 0 = 0 →
    ∀ (f : CompactlySupportedContinuousMap α β),
      (CompactlySupportedContinuousMap.compLeft g f).toContinuousMap = g.comp ↑f
-- Init.Data.List.Impl
List.insertIdx_eq_insertIdxTR : @List.insertIdx = @List.insertIdxTR
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.sum_measure : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [Countable ι] [inst : TopologicalSpace β] {f : α → β}
  [TopologicalSpace.PseudoMetrizableSpace β] {m : MeasurableSpace α} {μ : ι → MeasureTheory.Measure α},
  (∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ i)) →
    MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.sum μ)
-- Mathlib.Algebra.BigOperators.Finprod
finsum_of_isEmpty : ∀ {M : Type u_2} {α : Sort u_4} [inst : AddCommMonoid M] [IsEmpty α] (f : α → M), ∑ᶠ (i : α), f i = 0
-- Init.Core
/-- Type class used to implement the notation `{ a ∈ c | p a }`  -/
Sep : outParam (Type u) → Type v → Type (max u v)
-- Init.Data.Dyadic.Basic
Dyadic.zero_eq : Dyadic.zero = 0
-- Mathlib.NumberTheory.Divisors
Nat.properDivisors_subset_divisors : ∀ {n : ℕ}, n.properDivisors ⊆ n.divisors
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- For the identity map, all points are periodic.  -/
Function.is_periodic_id : ∀ {α : Type u_1} (n : ℕ) (x : α), Function.IsPeriodicPt id n x
-- Mathlib.Algebra.Module.Submodule.Range
/-- If `N ⊆ M` then submodules of `N` are the same as submodules of `M` contained in `N`.

See also `Submodule.mapIic`.  -/
Submodule.MapSubtype.orderIso : {R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (p : Submodule R M) → Submodule R ↥p ≃o { p' // p' ≤ p }
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.IsInvertedBy.iff_comp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (W : CategoryTheory.MorphismProperty C₁) (F : CategoryTheory.Functor C₁ C₂) (G : CategoryTheory.Functor C₂ C₃)
  [G.ReflectsIsomorphisms], W.IsInvertedBy (F.comp G) ↔ W.IsInvertedBy F
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcycles_ext_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] {A : C} (f₁ f₂ : S.opcycles ⟶ A),
  f₁ = f₂ ↔ CategoryTheory.CategoryStruct.comp S.pOpcycles f₁ = CategoryTheory.CategoryStruct.comp S.pOpcycles f₂
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_of_mem_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {f : α → Bool} {k : α},
  k ∈ Std.TreeSet.filter f t → k ∈ t
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivWithinAt.congr_mfderiv : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  {f' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt[s] f x f' → f' = f₁' → HasMFDerivAt[s] f x f₁'
-- Mathlib.CategoryTheory.Functor.Flat
/-- Being a representably flat functor is closed under natural isomorphisms.  -/
CategoryTheory.RepresentablyFlat.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [CategoryTheory.RepresentablyFlat F] {G : CategoryTheory.Functor C D} (α : F ≅ G),
  CategoryTheory.RepresentablyFlat G
-- Mathlib.RingTheory.SimpleRing.Defs
IsSimpleRing.simple : ∀ {R : Type u_1} {inst : NonUnitalNonAssocRing R} [self : IsSimpleRing R], IsSimpleOrder (TwoSidedIdeal R)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.IsReduced.infix : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.IsReduced L₂ → L₁ <:+: L₂ → FreeGroup.IsReduced L₁
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.forM_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} {m : Type w → Type w'}
  [Std.TransOrd α] [inst : Monad m] [LawfulMonad m],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {f : (a : α) → β a → m PUnit.{w + 1}},
          Std.DTreeMap.Internal.Impl.forM f t₁ = Std.DTreeMap.Internal.Impl.forM f t₂
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.op_i₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A),
  P.op.i₁ = P.p₁.op
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.e_inv_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.e F G X).inv.app X_1 = X_1.iso.inv
-- Mathlib.Analysis.LocallyConvex.Bounded
NormedSpace.image_isVonNBounded_iff : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {α : Type u_6} {f : α → E} {s : Set α},
  Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ r, ∀ x ∈ s, ‖f x‖ ≤ r
-- Init.Data.Int.Order
Int.sign_eq_zero_iff_zero : ∀ {a : ℤ}, a.sign = 0 ↔ a = 0
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- The free variable of the parameter created in a telescope for logging.
We always expect this to be `some _` normally, but allow `none` as a failsafe.  -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.Parameter.fvar? : Mathlib.Linter.UnusedInstancesInType.Parameter✝ → Option Lean.Expr
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
/-- Suppose `A` is an `R`-algebra, `M` is an `A`-module such that `a • m ≠ 0` for all non-zero `a`
and `m`. If `x : A` fixes a nontrivial f.g. `R`-submodule `N` of `M`, then `x` is `R`-integral.  -/
isIntegral_of_smul_mem_submodule : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [IsDomain A]
  {M : Type u_5} [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : Module A M] [IsScalarTower R A M]
  [Module.IsTorsionFree A M] (N : Submodule R M), N ≠ ⊥ → N.FG → ∀ (x : A), (∀ n ∈ N, x • n ∈ N) → IsIntegral R x
-- Std.Data.Internal.List.Associative
Std.Internal.List.Sigma.snd_congr : ∀ {α : Type u} {β : α → Type v} {x x' : (a : α) × β a} (h : x = x'), x.snd = cast ⋯ x'.snd
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Restrict a ring homomorphism with a left inverse to a ring isomorphism to its
`RingHom.range`.  -/
RingEquiv.ofLeftInverse : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocRing R] →
      [inst_1 : NonAssocRing S] → {g : S → R} → {f : R →+* S} → Function.LeftInverse g ⇑f → R ≃+* ↥f.range
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.stronglyMeasurable_stieltjesFunction : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : ProbabilityTheory.IsMeasurableRatCDF f) (x : ℝ),
  MeasureTheory.StronglyMeasurable fun a => ↑(hf.stieltjesFunction a) x
-- Mathlib.AlgebraicGeometry.Birational.Composition
/-- Composition respects equivalence of partial maps on the left.  -/
AlgebraicGeometry.Scheme.PartialMap.comp_equiv_of_equiv_left : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] {f₁ f₂ : X.PartialMap Y}
  [inst_2 : AlgebraicGeometry.IsDominant f₁.hom] [inst_3 : AlgebraicGeometry.IsDominant f₂.hom],
  f₁.equiv f₂ → ∀ (g : Y.PartialMap Z), (f₁.comp g).equiv (f₂.comp g)
-- Mathlib.Order.CompleteLattice.Basic
sSup_image : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {s : Set β} {f : β → α}, sSup (f '' s) = ⨆ a ∈ s, f a
-- Init.Data.Fin.Lemmas
Fin.induction_zero : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (zero : motive 0) (hs : (i : Fin n) → motive i.castSucc → motive i.succ),
  (fun i => Fin.induction zero hs i) 0 = zero
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Sort u} →
    {motive_3 : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Sort u} →
      {motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u} →
        {motive_5 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Sort u} →
          {motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u} →
            {motive_7 : Lean.Meta.Grind.Arith.Linear.UnsatProof → Sort u} →
              (t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) →
                ((t : Lean.Meta.Grind.Arith.Linear.EqCnstr) → t.below → motive_1 t) →
                  ((t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) → t.below → motive_2 t) →
                    ((t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) → t.below → motive_3 t) →
                      ((t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) → t.below → motive_4 t) →
                        ((t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) → t.below → motive_5 t) →
                          ((t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) → t.below → motive_6 t) →
                            ((t : Lean.Meta.Grind.Arith.Linear.UnsatProof) → t.below → motive_7 t) →
                              motive_2 t ×' t.below
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.coassoc_right_assoc : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid M']
  [inst_6 : Module R M'] [inst_7 : Coalgebra R M] (f : M →ₗ[R] M') (g : N →ₗ[R] M),
  ↑(TensorProduct.assoc R M' M M).symm ∘ₗ TensorProduct.map f CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul ∘ₗ g =
    TensorProduct.map (TensorProduct.map f LinearMap.id) LinearMap.id ∘ₗ
      TensorProduct.map CoalgebraStruct.comul LinearMap.id ∘ₗ CoalgebraStruct.comul ∘ₗ g
-- Aesop.Index.Basic
Aesop.IndexMatchResult.instLTOfOrd : {α : Type} → [Ord α] → LT (Aesop.IndexMatchResult α)
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `Distrib` instance along a surjective function.  -/
Function.Surjective.distrib : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Distrib R] →
              (∀ (x y : R), f (x + y) = f x + f y) → (∀ (x y : R), f (x * y) = f x * f y) → Distrib S
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.DoIfView.ref : Lean.Elab.Term.Do.DoIfView → Lean.Syntax
-- Mathlib.Data.Set.Basic
Set.inter_eq_inter_iff_left : ∀ {α : Type u} {s t u : Set α}, s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instNontrivial : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [Nontrivial R], Nontrivial (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.sSup_empty : ∀ (α : Type u_5) [inst : CompleteLattice α], sSup ∅ = ⊥
-- Lean.Environment
Lean.ConstantKind.ctor : Lean.ConstantKind
-- Mathlib.Logic.Equiv.Functor
Functor.mapEquiv_apply : ∀ {α β : Type u} (f : Type u → Type v) [inst : Functor f] [inst_1 : LawfulFunctor f] (h : α ≃ β) (x : f α),
  (Functor.mapEquiv f h) x = ⇑h <$> x
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.ofIsoColimit.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit r)
  (i : r ≅ t),
  P.ofIsoColimit i =
    CategoryTheory.Limits.IsColimit.mkCoconeMorphism
      (fun s => CategoryTheory.CategoryStruct.comp i.inv (P.descCoconeMorphism s)) ⋯
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The center of a semiring acts commutatively on any `R`-module  -/
Subring.instSMulCommClassSubtypeMemCenter : ∀ {R : Type u_3} {M : Type u_4} [inst : Ring R] [inst_1 : MulAction R M], SMulCommClass R (↥(Subring.center R)) M
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- The homogeneous degree bounds the total degree.

See also `MvPolynomial.IsHomogeneous.totalDegree` when `φ` is non-zero.  -/
MvPolynomial.IsHomogeneous.totalDegree_le : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ},
  φ.IsHomogeneous n → φ.totalDegree ≤ n
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.mapHomologicalComplexObjIso_inv_map_π₀_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  {D : Type u_3} [inst_5 : CategoryTheory.Category.{v_2, u_3} D] [inst_6 : CategoryTheory.Preadditive D]
  (H : CategoryTheory.Functor C D) [inst_7 : H.Additive]
  [inst_8 :
    ∀ (i : α),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.mapHomologicalComplex c).obj K).X i)
        (((H.mapHomologicalComplex c).obj K).X i)]
  [inst_9 : ((H.mapHomologicalComplex c).obj K).HasPathObject]
  [inst_10 :
    ∀ (i : α),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.op.mapHomologicalComplex c.symm).obj K.op).X i)
        (((H.op.mapHomologicalComplex c.symm).obj K.op).X i)]
  [inst_11 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift
        (CategoryTheory.CategoryStruct.id ((H.op.mapHomologicalComplex c.symm).obj K.op))
        (-CategoryTheory.CategoryStruct.id ((H.op.mapHomologicalComplex c.symm).obj K.op)))]
  [inst_12 :
    HomologicalComplex.HasHomotopyCofiber
      ((H.op.mapHomologicalComplex c.symm).map
        (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K.op)
          (-CategoryTheory.CategoryStruct.id K.op)))]
  [inst_13 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.op.X i) (K.op.X i)] (hc : ∀ (i : α), ∃ j, c.Rel i j)
  {Z : HomologicalComplex D c} (h : (H.mapHomologicalComplex c).obj K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.mapHomologicalComplexObjIso K H hc).inv
      (CategoryTheory.CategoryStruct.comp ((H.mapHomologicalComplex c).map (HomologicalComplex.pathObject.π₀ K)) h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.π₀ ((H.mapHomologicalComplex c).obj K)) h
-- Mathlib.CategoryTheory.Preadditive.Opposite
_private.Mathlib.CategoryTheory.Preadditive.Opposite.0.CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite.match_1.splitter : {C : Type u_2} →
  [inst : CategoryTheory.Category.{u_1, u_2} C] →
    (G : C) →
      (motive : (CategoryTheory.End G)ᵐᵒᵖ → Sort u_3) →
        (x : (CategoryTheory.End G)ᵐᵒᵖ) → ((f : CategoryTheory.End G) → motive { unop' := f }) → motive x