mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
FiniteMultiplicity.of_not_isUnit : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] [WfDvdMonoid α] {a b : α},
  ¬IsUnit a → b ≠ 0 → FiniteMultiplicity a b
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
/-- Left unitor for the vertical composition of oplax natural transformations.  -/
CategoryTheory.Oplax.OplaxTrans.leftUnitor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          (η : F ⟶ G) → CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id F) η ≅ η
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op.eq_1 : ∀ {M : Type u_2} [inst : AddZeroClass M] (x : AddSubmonoid M),
  x.op = { carrier := AddOpposite.unop ⁻¹' ↑x, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.equalizerSubobjectIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g],
  CategoryTheory.Limits.equalizerSubobjectIso f g =
    CategoryTheory.Subobject.underlyingIso (CategoryTheory.Limits.equalizer.ι f g)
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Icc_eq_Ici_self_iff : ∀ {ι : Sort u} {α : Type v} [inst : LinearOrder α] {f : ι → α} {a : α},
  ⋃ i, Set.Icc a (f i) = Set.Ici a ↔ ∀ x ≥ a, ∃ i, x ≤ f i
-- Batteries.Util.ProofWanted
/-- Shared elaborator for `theorem_wanted` and `def_wanted`. Walks the statement and (if
present) the body, rewriting each `❰x❱` to a fresh parameter; the parameter's type uses the
accessor (`ProofWanted.Stmt` or `DefWanted.Val`) appropriate to `x`'s own kind. If the
body has no `❰…❱` reference anywhere, emits a "Try this:" suggesting `theorem` / `def`.  -/
_private.Batteries.Util.ProofWanted.0.elabWanted : WantedCmdKind✝ →
  Lean.Syntax →
    Lean.TSyntax `Lean.Parser.Command.declModifiers →
      Lean.TSyntax `Lean.Parser.Command.declId →
        Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole, `Lean.Parser.Term.bracketedBinder] →
          Lean.TSyntax `term → Option (Lean.TSyntax `term) → Lean.Elab.Command.CommandElabM Unit
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_ofVar : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (x : Lean.Grind.CommRing.Var),
  Lean.Grind.CommRing.Poly.denoteS ctx (Lean.Grind.CommRing.Poly.ofVar x) = Lean.Grind.CommRing.Var.denote ctx x
-- Mathlib.Algebra.Notation.Support
Set.image_inter_support_eq : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Zero M] {f : ι → M} {s : Set κ} {g : κ → ι},
  g '' s ∩ Function.support f = g '' (s ∩ Function.support (f ∘ g))
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_uIcc_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Lattice (α i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (a : α i), Pi.mulSingle i '' Set.uIcc a 1 = Set.uIcc (Pi.mulSingle i a) 1
-- Mathlib.Algebra.Order.Field.Basic
lt_one_div : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α},
  0 < a → 0 < b → (a < 1 / b ↔ b < 1 / a)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.MkTableKey.M : Type → Type
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.HasBasis.uniformity_of_nhds_zero : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Sort u_3} {p : ι → Prop}
  {U : ι → Set α}, (nhds 0).HasBasis p U → (uniformity α).HasBasis p fun i => {x | x.2 - x.1 ∈ U i}
-- Mathlib.Analysis.Analytic.Within
/-- `f` has power series `p` at `x` iff some local extension of `f` has that series  -/
hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r ↔
    ∃ g, Set.EqOn f g (insert x s ∩ Metric.eball x r) ∧ HasFPowerSeriesOnBall g p x r
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.sub_prod_sub : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Ring R]
  [inst_1 : (i : ι) → AddCommGroup (M₁ i)] [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  [inst_7 : IsTopologicalAddGroup M₂] [inst_8 : AddCommGroup M₃] [inst_9 : Module R M₃] [inst_10 : TopologicalSpace M₃]
  [inst_11 : IsTopologicalAddGroup M₃] (f₁ f₂ : ContinuousMultilinearMap R M₁ M₂)
  (g₁ g₂ : ContinuousMultilinearMap R M₁ M₃), (f₁ - f₂).prod (g₁ - g₂) = f₁.prod g₁ - f₂.prod g₂
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressReport.mk.sizeOf_spec : ∀ (kind : String) (message? : Option String) (cancellable : Bool) (percentage? : Option ℕ),
  sizeOf { kind := kind, message? := message?, cancellable := cancellable, percentage? := percentage? } =
    1 + sizeOf kind + sizeOf message? + sizeOf cancellable + sizeOf percentage?
-- Mathlib.Geometry.Euclidean.Angle.Bisector
/-- A point `p` is equidistant to two different lines `p₁ p₂` and `p₁ p₃` if and only if the
oriented angles at `p₁` are equal modulo `π`.  -/
EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [inst_4 : Fact (Module.finrank ℝ V = 2)] [inst_5 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ p₃ : P},
  AffineIndependent ℝ ![p₁, p₂, p₃] →
    (dist p ↑((EuclideanGeometry.orthogonalProjection line[ℝ, p₁, p₂]) p) =
        dist p ↑((EuclideanGeometry.orthogonalProjection line[ℝ, p₁, p₃]) p) ↔
      2 • EuclideanGeometry.oangle p₂ p₁ p = 2 • EuclideanGeometry.oangle p p₁ p₃)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.unitOfList_eq_insertManyIfNewUnit_empty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α}, Std.HashMap.Raw.unitOfList l = ∅.insertManyIfNewUnit l
-- Init.System.IO
_private.Init.System.IO.0.BaseIO.mapTasks.go : {α : Type u_1} → {β : Type} → (List α → BaseIO β) → Task.Priority → Bool → List (Task α) → List α → BaseIO (Task β)
-- Mathlib.Data.DFinsupp.NeLocus
/-- Given two finitely supported functions `f g : α →₀ N`, `Finsupp.neLocus f g` is the `Finset`
where `f` and `g` differ. This generalizes `(f - g).support` to situations without subtraction.  -/
DFinsupp.neLocus : {α : Type u_1} →
  {N : α → Type u_2} →
    [DecidableEq α] →
      [(a : α) → DecidableEq (N a)] → [inst : (a : α) → Zero (N a)] → (Π₀ (a : α), N a) → (Π₀ (a : α), N a) → Finset α
-- Mathlib.Data.Set.Basic
Set.sep_true : ∀ {α : Type u} {s : Set α}, {x | x ∈ s ∧ True} = s
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.mk.sizeOf_spec : ∀ {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} [inst : SizeOf I₁]
  [inst_1 : SizeOf I₂] [inst_2 : SizeOf I₃] [inst_3 : SizeOf J] (I₂₃ : Type u_11) (p : I₂ × I₃ → I₂₃) (q : I₁ × I₂₃ → J)
  (hpq : ∀ (i : I₁ × I₂ × I₃), q (i.1, p i.2) = r i), sizeOf { I₂₃ := I₂₃, p := p, q := q, hpq := hpq } = 1 + sizeOf I₂₃
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- If `A` and `B` are isomorphic, then an ind-object presentation of `A` can be extended to an
ind-object presentation of `B`.  -/
CategoryTheory.Limits.IndObjectPresentation.extend : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      CategoryTheory.Limits.IndObjectPresentation A →
        (η : A ⟶ B) → [CategoryTheory.IsIso η] → CategoryTheory.Limits.IndObjectPresentation B
-- Mathlib.Algebra.Group.Prod
Prod.commMagma.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : CommMagma M] [inst_1 : CommMagma N],
  Prod.commMagma = { toMul := Prod.instMul, mul_comm := ⋯ }
-- Lean.Elab.PreDefinition.Basic
/-- Applies `Meta.letToHave` to the type of the predef.
 -/
Lean.Elab.letToHaveType : Lean.Elab.PreDefinition → Lean.MetaM Lean.Elab.PreDefinition
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- An elimination principle for `OnePoint`.  -/
OnePoint.elim : {X : Type u_1} → {Y : Type u_2} → OnePoint X → Y → (X → Y) → Y
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- Alternative phrasing of the normalizer condition: Only the full group is self-normalizing.
This may be easier to work with, as it avoids inequalities and negations.  -/
normalizerCondition_iff_only_full_group_self_normalizing : ∀ {G : Type u_1} [inst : Group G], NormalizerCondition G ↔ ∀ (H : Subgroup G), Subgroup.normalizer ↑H = H → H = ⊤
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
/-- Pull-out property of the conditional expectation.  -/
MeasureTheory.condExp_smul_of_aestronglyMeasurable_right : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : Ω → ℝ} {g : Ω → E},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable (f • g) μ → MeasureTheory.AEStronglyMeasurable g μ → μ[f • g | m] =ᵐ[μ] μ[f | m] • g
-- Init.Data.List.FinRange
List.finRange.eq_1 : ∀ (n : ℕ), List.finRange n = List.ofFn fun i => i
-- Mathlib.RingTheory.Etale.Kaehler
KaehlerDifferential.span_range_map_derivation_of_isLocalization : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] (M : Submonoid S)
  [IsLocalization M T],
  Submodule.span T (Set.range (⇑(KaehlerDifferential.map R R S T) ∘ ⇑(KaehlerDifferential.D R S))) = ⊤
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.le_mk_of_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} {X : CategoryTheory.Subobject B} {f : A ⟶ B}
  [inst_1 : CategoryTheory.Mono f] (g : CategoryTheory.Subobject.underlying.obj X ⟶ A),
  CategoryTheory.CategoryStruct.comp g f = X.arrow → X ≤ CategoryTheory.Subobject.mk f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instLaxMonoidalMonMapMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : CategoryTheory.BraidedCategory C] →
                [inst_5 : CategoryTheory.BraidedCategory D] → [inst_6 : F.LaxBraided] → F.mapMon.LaxMonoidal
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- If `c1` and `c2` both contain variable `a` with opposite coefficients,
produces `v1` and `v2` such that `a` has been cancelled in `v1*c1 + v2*c2`.  -/
Mathlib.Tactic.Linarith.elimVar : Mathlib.Tactic.Linarith.Comp → Mathlib.Tactic.Linarith.Comp → ℕ → Option (ℕ × ℕ)
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- Postcomposing a co-Cartesian morphism with an isomorphism lifting the identity is
co-Cartesian.  -/
CategoryTheory.Functor.IsCocartesian.of_comp_iso : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCocartesian f φ] {b' : 𝒳}
  (φ' : b ≅ b') [p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ'.hom],
  p.IsCocartesian f (CategoryTheory.CategoryStruct.comp φ φ'.hom)
-- Mathlib.MeasureTheory.Function.JacobianOneDim
/-- **Alias** of `MeasureTheory.integral_image_eq_integral_deriv_smul_of_antitoneOn`.

---

Change of variable formula for differentiable functions: if a real function `f` is
antitone and differentiable on a measurable set `s`, then the Bochner integral of a function
`g : ℝ → F` on `f '' s` coincides with the integral of `(-f' x) • g ∘ f` on `s` .  -/
MeasureTheory.integral_image_eq_integral_deriv_smul_of_antitone : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
      AntitoneOn f s → ∀ (g : ℝ → F), ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, -f' x • g (f x)
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Reinterpret a ring homomorphism `f : α →+* β` as an additive monoid homomorphism `α →+ β`.
The `simp`-normal form is `(f : α →+ β)`.  -/
RingHom.toAddMonoidHom : {α : Type u_5} → {β : Type u_6} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →+ β
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquivClass.instAddMonoidHomClass : ∀ (F : Type u_1) {M : Type u_4} {N : Type u_5} [inst : EquivLike F M N] [inst_1 : AddZeroClass M]
  [inst_2 : AddZeroClass N] [AddEquivClass F M N], AddMonoidHomClass F M N
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_expect_le : ∀ {K : Type u_1} {E : Type u_2} [inst : RCLike K] [inst_1 : NormedField E] [inst_2 : CharZero E] [NormedSpace K E]
  {ι : Type u_3} {s : Finset ι} {f : ι → E}, ‖s.expect fun i => f i‖ ≤ s.expect fun i => ‖f i‖
-- Lean.Parser.Command
Lean.Parser.Command.classTk : Lean.Parser.Parser
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.coe_top : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A : Set M} {α : Type u₁}, ↑⊤ = Set.univ
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.toBitVec_assemble₄Unchecked : ∀ {w x y z : UInt8},
  (ByteArray.utf8DecodeChar?.assemble₄Unchecked w x y z).toBitVec =
    BitVec.setWidth 32
      (BitVec.setWidth 3 w.toBitVec ++ BitVec.setWidth 6 x.toBitVec ++ BitVec.setWidth 6 y.toBitVec ++
        BitVec.setWidth 6 z.toBitVec)
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
/-- The (colimit) cocone which, for a point constructed using `Point.ofIsCofiltered`
and a functor `p : N ⥤ C` expresses the fiber of a presheaf as a colimit
indexed indexed by `N`.  -/
CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.LocallySmall.{w, v, u} C] →
      {N : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} N] →
          (p : CategoryTheory.Functor N C) →
            [CategoryTheory.InitiallySmall N] →
              {J : CategoryTheory.GrothendieckTopology C} →
                [CategoryTheory.IsCofiltered N] →
                  (∀ ⦃X : C⦄,
                      ∀ R ∈ J X,
                        ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
                          ∃ Y g,
                            ∃ (_ : R.arrows g),
                              ∃ V q a,
                                CategoryTheory.CategoryStruct.comp a g =
                                  CategoryTheory.CategoryStruct.comp (p.map q) f) →
                    {A : Type u''} →
                      [inst_5 : CategoryTheory.Category.{v'', u''} A] →
                        [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] →
                          (P : CategoryTheory.Functor Cᵒᵖ A) → CategoryTheory.Limits.Cocone (p.op.comp P)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.mem_invOf_smul_set : ∀ {α : Type u_2} {β : Type u_3} [inst : Monoid α] [inst_1 : MulAction α β] {s : Set β} {a : α} {b : β}
  [inst_2 : Invertible a], b ∈ ⅟a • s ↔ a • b ∈ s
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.star_subset_adjoin : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (s : Set A), star s ⊆ ↑(StarAlgebra.adjoin R s)
-- Mathlib.Analysis.Normed.Field.Basic
/-- The range of the norm is dense in the collection of nonnegative real numbers.  -/
DenselyNormedField.lt_norm_lt : ∀ {α : Type u_5} [self : DenselyNormedField α] (x y : ℝ), 0 ≤ x → x < y → ∃ a, x < ‖a‖ ∧ ‖a‖ < y
-- Mathlib.NumberTheory.Chebyshev
/-- Chebyshev's upper bound: `θ x ≤ c x` with the constant `c = log 4`.  -/
Chebyshev.theta_le_log4_mul_x : ∀ {x : ℝ}, 0 ≤ x → Chebyshev.theta x ≤ Real.log 4 * x
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_top : ↑⊤ = ⊤
-- Mathlib.Topology.Algebra.StarSubalgebra
StarSubalgebra.topologicalClosure_map : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A]
  [inst_6 : StarModule R A] [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A]
  [inst_9 : TopologicalSpace B] [inst_10 : Semiring B] [inst_11 : Algebra R B] [inst_12 : StarRing B]
  [inst_13 : StarModule R B] [inst_14 : IsSemitopologicalSemiring B] [inst_15 : ContinuousStar B]
  (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B),
  IsClosedMap ⇑φ →
    Continuous ⇑φ → (StarSubalgebra.map φ s).topologicalClosure = StarSubalgebra.map φ s.topologicalClosure
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.inv_hom_apply : ∀ {R S : SemiRingCat} (e : R ≅ S) (r : ↑R),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) r) = r
-- Init.Grind.ToInt
/-- The embedding into the integers is strictly monotone.
 -/
Lean.Grind.ToInt.LT : (α : Type u) → [LT α] → (I : outParam Lean.Grind.IntInterval) → [Lean.Grind.ToInt α I] → Prop
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
Float.Model.UnpackedFloat.pack.eq_def : ∀ (spec : Float.Model.Format) (x : Float.Model.UnpackedFloat),
  Float.Model.UnpackedFloat.pack spec x =
    match x with
    | Float.Model.UnpackedFloat.notANumber => Float.Model.UnpackedFloat.packedNaN spec
    | Float.Model.UnpackedFloat.infinity s => Float.Model.UnpackedFloat.packedInfinity spec s
    | Float.Model.UnpackedFloat.zero s => Float.Model.UnpackedFloat.packedZero spec s
    | Float.Model.UnpackedFloat.finite s m e mantissa_pos =>
      have actualMantissaBits := m.log2;
      have biasedExponent := (e + ↑spec.exponentBias + ↑spec.mantissaBitsWithoutImplicit).toNat;
      if 2 ^ spec.exponentBits ≤ biasedExponent + 1 then Float.Model.UnpackedFloat.packedInfinity spec s
      else
        if actualMantissaBits + 1 = spec.mantissaBits then
          Float.Model.UnpackedFloat.packComponents spec s (BitVec.ofNat spec.exponentBits biasedExponent)
            (BitVec.ofNat spec.mantissaBitsWithoutImplicit m)
        else
          Float.Model.UnpackedFloat.packComponents spec s (0#spec.exponentBits)
            (BitVec.ofNat spec.mantissaBitsWithoutImplicit m)
-- Lean.Compiler.Specialize
Lean.Compiler.instInhabitedSpecializeAttributeKind : Inhabited Lean.Compiler.SpecializeAttributeKind
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivAtFilter_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (c : F) (L : Filter (E × E)), HasFDerivAtFilter (fun x => c) 0 L
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constToList_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Internal.Impl.Const.toList t₁ = Std.DTreeMap.Internal.Impl.Const.toList t₂
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendXIso.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') {i' : ι'}
  {i : ι} (h : e.f i = i'), K.extendXIso e h = K.extendXIso e h
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instNonUnitalNonAssocRing : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [NonUnitalNonAssocRing R] → NonUnitalNonAssocRing (l.Germ R)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castSucc_uIoc_castSucc : ∀ {n : ℕ} (i j : Fin n), Fin.castSucc ⁻¹' Set.uIoc i.castSucc j.castSucc = Set.uIoc i j
-- Mathlib.Topology.MetricSpace.Cauchy
/-- In a pseudometric space, Cauchy sequences are characterized by the fact that, eventually,
the distance between its elements is arbitrarily small  -/
Metric.cauchySeq_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [Nonempty β] [inst_2 : SemilatticeSup β] {u : β → α},
  CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
-- Lean.Data.DeclarationRange
Lean.DeclarationRange.mk.sizeOf_spec : ∀ (pos : Lean.Position) (charUtf16 : ℕ) (endPos : Lean.Position) (endCharUtf16 : ℕ),
  sizeOf { pos := pos, charUtf16 := charUtf16, endPos := endPos, endCharUtf16 := endCharUtf16 } =
    1 + sizeOf pos + sizeOf charUtf16 + sizeOf endPos + sizeOf endCharUtf16
-- Mathlib.Algebra.Field.ModEq
AddCommGroup.mul_modEq_mul_left : ∀ {K : Type u_1} [inst : Semifield K] {a b c p : K}, c ≠ 0 → (c * a ≡ c * b [PMOD p] ↔ a ≡ b [PMOD p / c])
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M] {I : ModelWithCorners 𝕜 E H}
  [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] [inst_7 : TopologicalSpace H']
  [inst_8 : TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} {s : Set M} [inst_9 : ChartedSpace H M]
  [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M},
  ContinuousWithinAt f s x →
    nhdsWithin (↑(extChartAt I x) x) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) =
      nhdsWithin (↑(extChartAt I x) x)
        ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.map_nonunit' : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (self : MulChar R R') (a : R),
  ¬IsUnit a → (↑self.toMonoidHom).toFun a = 0
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Sheaves of modules on `𝒪_X` restricted to `U` are equivalent to sheaves of `𝒪_U`-modules.  -/
AlgebraicGeometry.Scheme.Modules.overEquiv : {X : AlgebraicGeometry.Scheme} →
  (U : X.Opens) → SheafOfModules (CategoryTheory.Sheaf.over X.ringCatSheaf U) ≌ (↑U).Modules
-- Mathlib.Order.Minimal
maximal_mem_Ioc : ∀ {α : Type u_2} {x : α} [inst : PartialOrder α] {a b : α}, b < a → (Maximal (fun x => x ∈ Set.Ioc b a) x ↔ x = a)
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.ofDigits_zmod : ∀ (b : ℤ) (k : ℕ) (L : List ℕ), Nat.ofDigits b L % ↑k = Nat.ofDigits (b % ↑k) L % ↑k
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.algebraMap_intNorm : ∀ {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_6} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [IsScalarTower A K L] [inst_10 : Algebra B L] [IsScalarTower A B L]
  [IsIntegralClosure B A L] [FiniteDimensional K L] [inst_14 : IsIntegrallyClosed A] [inst_15 : IsDomain A]
  [inst_16 : IsDomain B] [inst_17 : IsIntegrallyClosed B] [inst_18 : Algebra.IsIntegral A B]
  [inst_19 : Module.IsTorsionFree A B] (x : B),
  (algebraMap A K) ((Algebra.intNorm A B) x) = (Algebra.norm K) ((algebraMap B L) x)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_naturality_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  ((CategoryTheory.CategoryStruct.id F).naturality f).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom
      (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv