mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.MinMax
Array.foldl_min_eq_min : ∀ {α : Type u_1} [inst : Min α] [Std.IdempotentOp min] [Std.Associative min] {xs : Array α} (h : xs ≠ #[]) {a : α},
  Array.foldl min a xs = a ⊓ xs.min h
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
/-- `E2` is bounded at `i∞`.  -/
EisensteinSeries.isBoundedAtImInfty_E2 : UpperHalfPlane.IsBoundedAtImInfty EisensteinSeries.E2
-- Mathlib.Analysis.Seminorm
Seminorm.coe_iSup_eq : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {ι : Sort u_12}
  {p : ι → Seminorm 𝕜 E}, BddAbove (Set.range p) → ⇑(⨆ i, p i) = ⨆ i, ⇑(p i)
-- Mathlib.Topology.MetricSpace.Isometry
/-- An isometry from a metric space is a uniform continuous map  -/
Isometry.uniformContinuous : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → UniformContinuous f
-- Mathlib.GroupTheory.Solvable
derivedSeries_le_map_derivedSeries : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'},
  Function.Surjective ⇑f → ∀ (n : ℕ), derivedSeries G' n ≤ Subgroup.map f (derivedSeries G n)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
/-- A weak equalizer cone for a parallel pair `f` and `g`  -/
CategoryTheory.Limits.weakEqualizer.fork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} → (f g : X ⟶ Y) → [CategoryTheory.Limits.HasWeakEqualizer f g] → CategoryTheory.Limits.Fork f g
-- Mathlib.CategoryTheory.Localization.Bifunctor
/-- The natural transformation `F₁' ⟶ F₂'` of bifunctors induced by a
natural transformation `τ : F₁ ⟶ F₂` when `Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'`
and `Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'` hold.  -/
CategoryTheory.Localization.lift₂NatTrans : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          [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} D₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] →
                    (L₁ : CategoryTheory.Functor C₁ D₁) →
                      (L₂ : CategoryTheory.Functor C₂ D₂) →
                        (W₁ : CategoryTheory.MorphismProperty C₁) →
                          (W₂ : CategoryTheory.MorphismProperty C₂) →
                            [L₁.IsLocalization W₁] →
                              [L₂.IsLocalization W₂] →
                                [W₁.ContainsIdentities] →
                                  [W₂.ContainsIdentities] →
                                    (F₁ F₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) →
                                      (F₁' F₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) →
                                        [CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'] →
                                          [CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'] →
                                            (F₁ ⟶ F₂) → (F₁' ⟶ F₂')
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.succ_one : Order.succ 1 = 2
-- Mathlib.LinearAlgebra.Matrix.Notation
/-- Use `![...]` notation for displaying a `Fin`-indexed matrix, for example:

```
#eval !![1, 2; 3, 4] + !![3, 4; 5, 6]  -- !![4, 6; 8, 10]
```
 -/
Matrix.repr : {α : Type u} → {n m : ℕ} → [Repr α] → Repr (Matrix (Fin m) (Fin n) α)
-- Mathlib.Analysis.LConvolution
/-- The convolution of `AEMeasurable` functions is `AEMeasurable`.  -/
MeasureTheory.aemeasurable_lconvolution : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] {f g : G → ENNReal},
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (MeasureTheory.lconvolution f g μ) μ
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The composition functor is also the composition on additive group objects.  -/
CategoryTheory.Functor.mapAddGrpCompIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.CartesianMonoidalCategory E] →
                  {F : CategoryTheory.Functor C D} →
                    {G : CategoryTheory.Functor D E} →
                      [inst_6 : F.Monoidal] →
                        [inst_7 : G.Monoidal] → (F.comp G).mapAddGrp ≅ F.mapAddGrp.comp G.mapAddGrp
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.mem_range_toGeneralLinearGroup_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  {u : LinearMap.GeneralLinearGroup R V},
  u ∈ Set.range ⇑SpecialLinearGroup.toGeneralLinearGroup ↔ LinearEquiv.det u.toLinearEquiv = 1
-- Std.Time.Format.Modifier
Std.Time.instInhabitedText : Inhabited Std.Time.Text
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instNegOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : Neg Mᵃᵒᵖ], DomAddAct.instNegOfAddOpposite = inst
-- Mathlib.Algebra.Order.Star.Basic
star_lt_one_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R] {x : R},
  star x < 1 ↔ x < 1
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- A `SavedLocalContext` captures the state and local context of a `MetaM`, to be continued later.
 -/
Lean.Elab.WF.GuessLex.SavedLocalContext : Type
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addIndex_mono : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {K K' V : Set G},
  IsCompact K' →
    K ⊆ K' → (interior V).Nonempty → MeasureTheory.Measure.haar.addIndex K V ≤ MeasureTheory.Measure.haar.addIndex K' V
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of the reverse direction of `Submodule.projection_apply_eq_zero_iff`. -/
Submodule.projection_apply_of_mem_right : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) {x : E}, x ∈ q → (p.projection q hpq) x = 0
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (L : Type u_3) [inst_2 : Field L] [inst_3 : Algebra K L]
  [inst_4 : Finite L], Function.Bijective fun n => FiniteField.frobeniusAlgEquivOfAlgebraic K L ^ ↑n
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Under.forgetMapInitial_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) {I : C} (hI : CategoryTheory.Limits.IsInitial I)
  (X_1 : CategoryTheory.Under X),
  (CategoryTheory.Under.forgetMapInitial X hI).hom.app X_1 = CategoryTheory.CategoryStruct.id X_1.right
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
/-- Closure of a family of elements of a presheaf under restriction and gluing of
sections over coverings in `K`.  -/
CategoryTheory.Precoverage.SubsheafClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Precoverage C →
      {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
        ((Z : C) → Set (F.obj (Opposite.op Z))) → (Z : C) → F.obj (Opposite.op Z) → Prop
-- Mathlib.SetTheory.Ordinal.Notation
ONote.oadd_add : ∀ (e : ONote) (n : ℕ+) (a o : ONote), e.oadd n a + o = e.addAux n (a + o)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.instCompactSpaceNNReal : ∀ {A : Type u_3} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] (a : A) [CompactSpace ↑(spectrum ℝ a)],
  CompactSpace ↑(spectrum NNReal a)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LVal.getRef : Lean.Elab.Term.LVal → Lean.Syntax
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.diff!_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₃.WF → m₁.Equiv m₂ → (m₁.diff! m₃).Equiv (m₂.diff! m₃)
-- Mathlib.Order.Filter.CardinalInter
/-- Every `CardinalInterFilter` for some `c` also is a `CardinalInterFilter` for any `a ≤ c`.  -/
CardinalInterFilter.of_cardinalInterFilter_of_le : ∀ {α : Type u} {c : Cardinal.{u}} (l : Filter α) [CardinalInterFilter l c] {a : Cardinal.{u}},
  a ≤ c → CardinalInterFilter l a
-- Lean.Parser.Term
Lean.Parser.Term.letOptUsedOnly.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_eq_zero_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α}, s.gcd f = 0 ↔ ∀ x ∈ s, f x = 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.let.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (decl : Lean.Compiler.LCNF.LetDecl pu) (k : Lean.Compiler.LCNF.Code pu)
  (decl_1 : Lean.Compiler.LCNF.LetDecl pu) (k_1 : Lean.Compiler.LCNF.Code pu),
  (Lean.Compiler.LCNF.Code.let decl k = Lean.Compiler.LCNF.Code.let decl_1 k_1) = (decl = decl_1 ∧ k = k_1)
-- Std.Do.WP.Basic
Std.Do.State.instWP : {σ : Type u_1} → Std.Do.WP (StateM σ) (Std.Do.PostShape.arg σ Std.Do.PostShape.pure)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_map_equiv : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f : R ≃+* S} {K : Subsemiring R}
  {x : S}, x ∈ Subsemiring.map (↑f) K ↔ f.symm x ∈ K
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Unitization.quasispectrum_inr_eq : ∀ (R : Type u_3) (S : Type u_4) {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Algebra R S] [inst_4 : Module S A] [inst_5 : IsScalarTower S A A] [inst_6 : SMulCommClass S A A]
  [inst_7 : Module R A] [IsScalarTower R S A] (a : A), quasispectrum R ↑a = quasispectrum R a
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_add_not_infinite : ∀ {x y : ℝ*}, x.InfinitePos → ¬y.Infinite → (x + y).InfinitePos
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.commRingNorm : Lean.Meta.Grind.Arith.Cutsat.LeCnstr →
  Lean.Meta.Grind.Arith.CommRing.RingExpr → Lean.Grind.CommRing.Poly → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Mathlib.Analysis.Convex.MetricSpace
Convexity.IsConvexDist.submodule : ∀ {F : Type u_3} {M : Type u_4} [inst : AddCommGroup M] [inst_1 : MetricSpace M] [inst_2 : Module ℝ M]
  [inst_3 : Convexity.ConvexSpace ℝ M] [inst_4 : Convexity.IsModuleConvexSpace ℝ M] [Convexity.IsConvexDist M]
  [inst_6 : SetLike F M] [inst_7 : AddSubmonoidClass F M] [inst_8 : SMulMemClass F ℝ M] {S : F},
  Convexity.IsConvexDist ↥S
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.branch.injEq : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (a : σ → Bool) (a_1 a_2 : Turing.TM2.Stmt Γ Λ σ)
  (a_3 : σ → Bool) (a_4 a_5 : Turing.TM2.Stmt Γ Λ σ),
  (Turing.TM2.Stmt.branch a a_1 a_2 = Turing.TM2.Stmt.branch a_3 a_4 a_5) = (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Std.Http.Data.Status
Std.Http.Status.requestHeaderFieldsTooLarge.sizeOf_spec : sizeOf Std.Http.Status.requestHeaderFieldsTooLarge = 1
-- Mathlib.Tactic.GCongr.Core
/-- The data for a "main" hypothesis of a `gcongr` lemma.
That is a hypothesis of the form `∀ xs, a xs' ~ b xs'` where `xs'` is a subset of `xs`,
and `a` and `b` form a "varying pair" in the conclusion of the `gcongr` lemma.  -/
Mathlib.Tactic.GCongr.GCongrHyp : Type
-- Init.Data.Vector.Lemmas
Vector.or_all_distrib_right : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool} {q : Bool}, (xs.all p || q) = xs.all fun a => p a || q
-- Mathlib.Algebra.Torsor.Defs
/-- Cancellation subtracting the results of two subtractions.  -/
vsub_sub_vsub_cancel_right : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p₁ p₂ p₃ : P), p₁ -ᵥ p₃ - (p₂ -ᵥ p₃) = p₁ -ᵥ p₂
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.descCocycle.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α α_1 : CochainComplex.HomComplex.Cochain K M m) (e_α : α = α_1)
  (β β_1 : CochainComplex.HomComplex.Cocycle L M n) (e_β : β = β_1) (h : m + 1 = n)
  (hαβ : CochainComplex.HomComplex.δ m n α + m.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0),
  CochainComplex.mappingCocone.descCocycle φ α β h hαβ = CochainComplex.mappingCocone.descCocycle φ α_1 β_1 h ⋯
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.IsG2.toIsValuedIn : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N} [self : P.IsG2],
  P.IsValuedIn ℤ
-- Mathlib.Data.Rel
SetRel.self_subset_image : ∀ {α : Type u_1} {R : SetRel α α} [R.IsRefl] (s : Set α), s ⊆ R.image s
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.im : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : RCLike 𝕜] {f : α → 𝕜},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun x => RCLike.im (f x)) μ
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_mk' : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →+* B) (h : ∀ (c : R) (x : A), f (c • x) = c • f x),
  ⇑(AlgHom.mk' f h) = ⇑f
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
LinearIndependent.span_eq_top_of_card_eq_finrank' : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1}
  [inst_3 : Fintype ι] [FiniteDimensional K V] {b : ι → V},
  LinearIndependent K b → Fintype.card ι = Module.finrank K V → Submodule.span K (Set.range b) = ⊤
-- Mathlib.Algebra.BigOperators.Fin
List.prod_ofFn : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} {f : Fin n → M}, (List.ofFn f).prod = ∏ i, f i
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Given `I : S.Arrow` and a morphism `g : Z ⟶ I.Y`, this is the arrow in `S.Arrow`
corresponding to `g ≫ I.f`.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.precomp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} → {S : J.Cover X} → (I : S.Arrow) → {Z : C} → (Z ⟶ I.Y) → S.Arrow
-- Lean.Meta.Tactic.Cases
Lean.Meta.GeneralizeIndicesSubgoal.mk.sizeOf_spec : ∀ (mvarId : Lean.MVarId) (indicesFVarIds : Array Lean.FVarId) (fvarId : Lean.FVarId) (numEqs : ℕ),
  sizeOf { mvarId := mvarId, indicesFVarIds := indicesFVarIds, fvarId := fvarId, numEqs := numEqs } =
    1 + sizeOf mvarId + sizeOf indicesFVarIds + sizeOf fvarId + sizeOf numEqs
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.piIsoPi_inv_π_apply : ∀ {ι : Type v} (α : ι → TopCat) (i : ι) (x : (i : ι) → ↑(α i)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π α i))
      ((CategoryTheory.ConcreteCategory.hom (TopCat.piIsoPi α).inv) x) =
    x i
-- Mathlib.Algebra.Group.Semiconj.Basic
SemiconjBy.zpow_right : ∀ {G : Type u_1} [inst : Group G] {a x y : G}, SemiconjBy a x y → ∀ (m : ℤ), SemiconjBy a (x ^ m) (y ^ m)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.maxEntryD.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3)
  (fallback : α × β) (h_1 : (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      (fallback : α × β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fallback) =
    h_1 fallback
-- Mathlib.Algebra.Order.Floor.Div
/-- Flooring division. If `a > 0`, then `b ⌊/⌋ a` is the greatest `c` such that `a • c ≤ b`.  -/
FloorDiv.floorDiv : {α : Type u_2} →
  {β : Type u_3} →
    {inst : AddCommMonoid α} →
      {inst_1 : PartialOrder α} →
        {inst_2 : AddCommMonoid β} →
          {inst_3 : PartialOrder β} → {inst_4 : SMulZeroClass α β} → [self : FloorDiv α β] → β → α → β
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.tendsto_nhds_bot_iff_real : ∀ {α : Type u_2} {m : α → EReal} {f : Filter α}, Filter.Tendsto m f (nhds ⊥) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, m a < ↑x
-- Mathlib.Algebra.Group.Subsemigroup.Operations
_private.Mathlib.Algebra.Group.Subsemigroup.Operations.0.MulHom.srange_mk_aux_mul : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M → N},
  (∀ (x y : M), f (x * y) = f x * f y) → ∀ {x y : N}, x ∈ Set.range f → y ∈ Set.range f → x * y ∈ Set.range f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point.0.termZ : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- Given an inequality `S₁ ≤ S₂` between subcomplexes of a simplicial set,
this is the induced morphism in the category `SSet`.  -/
SSet.Subcomplex.homOfLE : {X : SSet} → {S₁ S₂ : X.Subcomplex} → S₁ ≤ S₂ → (S₁.toSSet ⟶ S₂.toSSet)
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.instCoeSortType.eq_1 : MagmaCat.instCoeSortType = { coe := MagmaCat.carrier }
-- Lean.Parser.Extension
Lean.Parser.getBinaryAlias : {α : Type} → IO.Ref (Lean.Parser.AliasTable α) → Lean.Name → IO (α → α → α)
-- Mathlib.Data.Set.Opposite
Set.opEquiv_self_symm_apply_coe : ∀ {α : Type u_1} (s : Set α) (x : ↑s), ↑(s.opEquiv_self.symm x) = Opposite.op ↑x
-- Lean.Elab.PreDefinition.TerminationMeasure
/-- Elaborated form for a `termination_by` clause.

The `fn` has the same (value) arity as the recursive functions (stored in
`arity`), and maps its measures (including fixed prefix, in unpacked form) to
the termination measure.

If `structural := Bool`, then the `fn` is a lambda picking out exactly one measure.
 -/
Lean.Elab.TerminationMeasure : Type
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addY_of_X_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q →
      P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → W'.addY P Q * (P 2 * Q 2) ^ 3 = (-(P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3)) ^ 3
-- Mathlib.Probability.Decision.Risk.Basic
ProbabilityTheory.bayesRisk_of_subsingleton : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [Subsingleton 𝓧] [Nonempty 𝓨] [ProbabilityTheory.IsMarkovKernel P] [MeasureTheory.SFinite π],
  Measurable (Function.uncurry ℓ) → ProbabilityTheory.bayesRisk ℓ P π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π
-- Init.Grind.AC
Lean.Grind.AC.eq_norm_a : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op} (lhs rhs : Lean.Grind.AC.Expr)
  (lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_norm_a_cert lhs rhs lhs' rhs' = true →
    Lean.Grind.AC.Expr.denote ctx lhs = Lean.Grind.AC.Expr.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx lhs' = Lean.Grind.AC.Seq.denote ctx rhs'
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.toSubmodule_iSup : ∀ {ι : Sort u_1} {R : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid N]
  [inst_2 : TopologicalSpace N] [inst_3 : Module R N] [inst_4 : ContinuousAdd N] [inst_5 : ContinuousConstSMul R N]
  (f : ι → ClosedSubmodule R N), ↑(⨆ i, f i) = ↑(⨆ i, ↑(f i)).closure
-- Aesop.Tree.Data
Aesop.GoalUnsafe.brecOn.go : {motive_1 : Aesop.GoalUnsafe → Sort u} →
  {motive_2 : Aesop.MVarClusterUnsafe → Sort u} →
    {motive_3 : Aesop.RappUnsafe → Sort u} →
      {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u} →
        {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u} →
          {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u} →
            {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} →
              {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u} →
                {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} →
                  {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} →
                    {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} →
                      {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u} →
                        {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} →
                          (t : Aesop.GoalUnsafe) →
                            ((t : Aesop.GoalUnsafe) → t.below → motive_1 t) →
                              ((t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t) →
                                ((t : Aesop.RappUnsafe) → t.below → motive_3 t) →
                                  ((t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) →
                                      Aesop.GoalUnsafe.below_1 t → motive_4 t) →
                                    ((t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) →
                                        Aesop.GoalUnsafe.below_2 t → motive_5 t) →
                                      ((t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) →
                                          Aesop.GoalUnsafe.below_3 t → motive_6 t) →
                                        ((t : Array (IO.Ref Aesop.RappUnsafe)) →
                                            Aesop.GoalUnsafe.below_4 t → motive_7 t) →
                                          ((t : Option (IO.Ref Aesop.RappUnsafe)) →
                                              Aesop.GoalUnsafe.below_5 t → motive_8 t) →
                                            ((t : Array (IO.Ref Aesop.GoalUnsafe)) →
                                                Aesop.GoalUnsafe.below_6 t → motive_9 t) →
                                              ((t : Array (IO.Ref Aesop.MVarClusterUnsafe)) →
                                                  Aesop.GoalUnsafe.below_7 t → motive_10 t) →
                                                ((t : List (IO.Ref Aesop.RappUnsafe)) →
                                                    Aesop.GoalUnsafe.below_8 t → motive_11 t) →
                                                  ((t : List (IO.Ref Aesop.GoalUnsafe)) →
                                                      Aesop.GoalUnsafe.below_9 t → motive_12 t) →
                                                    ((t : List (IO.Ref Aesop.MVarClusterUnsafe)) →
                                                        Aesop.GoalUnsafe.below_10 t → motive_13 t) →
                                                      motive_1 t ×' t.below
-- Mathlib.RingTheory.Congruence.Hom
/-- The **second isomorphism theorem for rings**.  -/
RingCon.comapQuotientEquivRange : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Ring M] →
      [inst_1 : Ring N] →
        (c : RingCon M) → (f : N →+* M) → {d : RingCon N} → d = c.comap f → d.Quotient ≃+* ↥(c.mk'.comp f).range