mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.MinMax
List.maximum_eq_coe_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {m : α}, l.maximum = ↑m ↔ m ∈ l ∧ ∀ a ∈ l, a ≤ m
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_dist_center' : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (c x : P), EuclideanGeometry.inversion c (dist c x) x = x
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise scalar multiplication of `f` and
`g`, which antivary together on `s`, is unchanged by a permutation if and only if `f ∘ σ` and `g`
antivary together on `s`. Stated by permuting the entries of `f`.  -/
AntivaryOn.sum_comp_perm_smul_eq_sum_smul_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
  AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g i ↔ AntivaryOn (f ∘ ⇑σ) g ↑s)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- Given a family of morphisms `f : X i ⟶ S` and `f' : X' j ⟶ S'`, and suitable
commutative diagrams `p' j ≫ f (α j) = f' j ≫ p`, this is the
induced functor `F.DescentData f ⥤ F.DescentData f'`. (Up to a (unique) isomorphism,
this functor only depends on `f` and `f'`, see `pullFunctorIso`.)  -/
CategoryTheory.Pseudofunctor.DescentData.pullFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {S' : C} →
                {p : S' ⟶ S} →
                  {ι' : Type t'} →
                    {X' : ι' → C} →
                      {f' : (j : ι') → X' j ⟶ S'} →
                        {α : ι' → ι} →
                          {p' : (j : ι') → X' j ⟶ X (α j)} →
                            (∀ (j : ι'),
                                CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) =
                                  CategoryTheory.CategoryStruct.comp (f' j) p) →
                              CategoryTheory.Functor (F.DescentData f) (F.DescentData f')
-- Mathlib.Order.KrullDimension
Order.height_eq_of_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  StrictMono f → (∀ (a : α), ∀ b < f a, ∃ a' < a, f a' = b) → ∀ (a : α), Order.height a = Order.height (f a)
-- Mathlib.Topology.Algebra.Star.Real
NNReal.instContinuousStar : ContinuousStar NNReal
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
Module.Basis.addHaar_reindex : ∀ {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [inst : Fintype ι] [inst_1 : Fintype ι'] [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] (b : Module.Basis ι ℝ E) (e : ι ≃ ι'),
  (b.reindex e).addHaar = b.addHaar
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.right_inv : ∀ {R : Type u_5} [inst : CommSemiring R] {A : Type u_6} {B : Type u_7} [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (self : A ≃ₗc[R] B), Function.RightInverse self.invFun self.toFun
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Nat.toUInt16 5 = 5`
* `Nat.toUInt16 255 = 255`
* `Nat.toUInt16 32770 = 32770`
* `Nat.toUInt16 65537 = 1`
 -/
Nat.toUInt16 : ℕ → UInt16
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A constant multiplier of the weights in `weightedVSub_of` may be moved outside the sum.  -/
Finset.weightedVSub_const_smul : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (c : k),
  (s.weightedVSub p) (c • w) = c • (s.weightedVSub p) w
-- Std.Async.Basic
/-- Block until the `Async` finishes and returns its value. Propagates any error encountered during execution.
 -/
Std.Async.Async.block : {α : Type} → Std.Async.Async α → optParam Task.Priority Task.Priority.default → IO α
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.orthogonal_rootSpan_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [P.IsAnisotropic], P.RootForm.orthogonal (P.rootSpan R) = LinearMap.ker P.RootForm
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.forall_lt_mul : ∀ {b c : Ordinal.{u_4}} {P : Ordinal.{u_4} → Prop}, (∀ a < b * c, P a) ↔ ∀ q < c, ∀ r < b, P (b * q + r)
-- Mathlib.Topology.CompactOpen
/-- The uncurried form of a continuous map `X → C(Y, Z)` as a continuous map `X × Y → Z` (if `Y` is
locally compact). If `X` is also locally compact, then this is a homeomorphism between the two
function spaces, see `Homeomorph.curry`.  -/
ContinuousMap.uncurry : {X : Type u_2} →
  {Y : Type u_3} →
    {Z : Type u_4} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] → [LocallyCompactSpace Y] → C(X, C(Y, Z)) → C(X × Y, Z)
-- Mathlib.Topology.Order.LiminfLimsup
/-- A continuous monotone function between (conditionally) complete linear ordered spaces sends a
`Filter.limsup` to the `Filter.limsup` of the images (if the filter is bounded from above and
frequently bounded from below).  -/
Monotone.map_limsup_of_continuousAt : ∀ {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [F.NeBot] [inst : ConditionallyCompleteLinearOrder R]
  [inst_1 : TopologicalSpace R] [OrderTopology R] [inst_3 : ConditionallyCompleteLinearOrder S]
  [inst_4 : TopologicalSpace S] [OrderTopology S] {f : R → S},
  Monotone f →
    ∀ (a : ι → R),
      ContinuousAt f (Filter.limsup a F) →
        autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F a) Monotone.map_limsup_of_continuousAt._auto_1 →
          autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F a) Monotone.map_limsup_of_continuousAt._auto_3 →
            f (Filter.limsup a F) = Filter.limsup (f ∘ a) F
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.insertListₘ.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β)
  (hd : (a : α) × β a) (tl : List ((a : α) × β a)), m.insertListₘ (hd :: tl) = (m.insert hd.fst hd.snd).insertListₘ tl
-- Mathlib.Topology.Clopen
/-- The intersection of a disjoint covering by two open sets of a clopen set will be clopen.  -/
isClopen_inter_of_disjoint_cover_clopen : ∀ {X : Type u} [inst : TopologicalSpace X] {s a b : Set X},
  IsClopen s → s ⊆ a ∪ b → IsOpen a → IsOpen b → Disjoint a b → IsClopen (s ∩ a)
-- Init.Data.List.Nat.Range
List.count_range : ∀ {a n : ℕ}, List.count a (List.range n) = if a < n then 1 else 0
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.coe_finsuppScalarRight' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {ι : Type u_5}
  [inst_7 : DecidableEq ι], ⇑(TensorProduct.finsuppScalarRight R S M ι) = ⇑(TensorProduct.finsuppScalarRight R S M ι)
-- Aesop.Tree.State
Aesop.GoalRef.markUnprovable : Aesop.GoalRef → BaseIO Unit
-- Mathlib.Order.Max
noMaxOrder_of_left : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [NoMaxOrder α], NoMaxOrder (α × β)
-- Lean.Elab.Do.Control
Lean.Elab.Do.EffectForwarder.mk.injEq : ∀ (origCont : Lean.Elab.Do.DoElemCont) (returnBase? breakBase? continueBase? : Option Lean.Elab.Do.ControlStack)
  (liftedStack : Lean.Elab.Do.ControlStack) (liftedDoBlockResultType : Lean.Expr) (origCont_1 : Lean.Elab.Do.DoElemCont)
  (returnBase?_1 breakBase?_1 continueBase?_1 : Option Lean.Elab.Do.ControlStack)
  (liftedStack_1 : Lean.Elab.Do.ControlStack) (liftedDoBlockResultType_1 : Lean.Expr),
  ({ origCont := origCont, returnBase? := returnBase?, breakBase? := breakBase?, continueBase? := continueBase?,
        liftedStack := liftedStack, liftedDoBlockResultType := liftedDoBlockResultType } =
      { origCont := origCont_1, returnBase? := returnBase?_1, breakBase? := breakBase?_1,
        continueBase? := continueBase?_1, liftedStack := liftedStack_1,
        liftedDoBlockResultType := liftedDoBlockResultType_1 }) =
    (origCont = origCont_1 ∧
      returnBase? = returnBase?_1 ∧
        breakBase? = breakBase?_1 ∧
          continueBase? = continueBase?_1 ∧
            liftedStack = liftedStack_1 ∧ liftedDoBlockResultType = liftedDoBlockResultType_1)
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_else_not_ite' : ∀ (c0 c1 : Bool) {a b : Bool}, (bif c0 then a else !bif c1 then !a else b) = bif !c0 && !c1 then !b else a
-- Mathlib.Algebra.Lie.Basic
LieHom.id_comp : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂), LieHom.id.comp f = f
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Origin.lt : Lean.Meta.Origin → Lean.Meta.Origin → Bool
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_add_int' : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddGroupWithOne G]
  [inst_2 : AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℤ), f (x + ↑n) = f x + n • b
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.Reorder.mk : Mathlib.Tactic.Translate.Permutation → Mathlib.Tactic.Translate.ArgReorder → Mathlib.Tactic.Translate.Reorder
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner
MeasureTheory.AEStronglyMeasurable.const_inner : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → E} {c : E},
  MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun x => inner 𝕜 c (g x)) μ
-- Mathlib.Algebra.Group.Center
/-- associative property for right multiplication  -/
IsMulCentral.right_assoc : ∀ {M : Type u_1} [inst : Mul M] {z : M}, IsMulCentral z → ∀ (a b : M), a * b * z = a * (b * z)
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
/-- Given a short exact complex `S` in `C` that is short exact (`hS`), this is the
canonical isomorphism between the triangle `hS.singleTriangle` in the derived category
and the triangle attached to the corresponding short exact sequence of cochain complexes
after the application of the single functor.  -/
CategoryTheory.ShortComplex.ShortExact.singleTriangleIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        {S : CategoryTheory.ShortComplex C} → (hS : S.ShortExact) → hS.singleTriangle ≅ DerivedCategory.triangleOfSES ⋯
-- Mathlib.Algebra.Group.Subgroup.Even
/-- In a commutative semigroup `S`, `Subsemigroup.square S` is the subsemigroup of squares in `S`.
 -/
Subsemigroup.square : (S : Type u_1) → [inst : CommSemigroup S] → Subsemigroup S
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
Std.Iter.val_step_dropWhile : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {P : β → Bool} {it : Std.Iter β},
  ↑(Std.Iter.dropWhile P it).step =
    match ↑it.step with
    | Std.IterStep.yield it' out =>
      match P out with
      | true => Std.IterStep.skip (Std.Iter.Intermediate.dropWhile P true it')
      | false => Std.IterStep.yield (Std.Iter.Intermediate.dropWhile P false it') out
    | Std.IterStep.skip it' => Std.IterStep.skip (Std.Iter.Intermediate.dropWhile P true it')
    | Std.IterStep.done => Std.IterStep.done
-- Mathlib.CategoryTheory.EssentialImage
/-- Lift a functor `G : J ⥤ D` to the essential image of a fully faithful functor `F : C ⥤ D` to a
functor `G' : J ⥤ C` such that `G' ⋙ F ≅ G`. See `essImage.liftFunctorCompIso`.  -/
CategoryTheory.Functor.essImage.liftFunctor : {J : Type u_1} →
  {C : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} J] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            (G : CategoryTheory.Functor J D) →
              (F : CategoryTheory.Functor C D) →
                [F.Full] → [F.Faithful] → (∀ (j : J), F.essImage (G.obj j)) → CategoryTheory.Functor J C
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f f_1 : X ⟶ Y) (e_f : f = f_1)
  [inst_1 : CategoryTheory.Limits.HasImage f], CategoryTheory.Limits.image f = CategoryTheory.Limits.image f_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_eq_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α}
  {fallback : β} {h : a ∈ t}, Std.DTreeMap.Const.get t a h = Std.DTreeMap.Const.getD t a fallback
-- Mathlib.Data.Set.Lattice
Set.symmDiff_sUnion_subset : ∀ {α : Type u_1} {s : Set α} {S : Set (Set α)}, S.Nonempty → symmDiff s (⋃₀ S) ⊆ ⋃₀ ((fun x => symmDiff s x) '' S)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.size + t₂.size = (t₁ ∪ t₂).size + (t₁ ∩ t₂).size
-- Mathlib.Algebra.Star.RingQuot
_private.Mathlib.Algebra.Star.RingQuot.0.RingQuot.star'_quot : ∀ {R : Type u} [inst : Semiring R] (r : R → R → Prop) [inst_1 : StarRing R]
  (hr : ∀ (a b : R), r a b → r (star a) (star b)) {a : R},
  RingQuot.star'✝ r hr { toQuot := Quot.mk (RingQuot.Rel r) a } = { toQuot := Quot.mk (RingQuot.Rel r) (star a) }
-- Mathlib.Algebra.Group.Prod
Prod.instCommMonoid.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : CommMonoid M] [inst_1 : CommMonoid N],
  Prod.instCommMonoid = { toMonoid := Prod.instMonoid, mul_comm := ⋯ }
-- Mathlib.Data.Vector.Basic
List.Vector.toList_tail : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n), v.tail.toList = v.toList.tail
-- Mathlib.Data.ENat.Basic
ENat.add_lt_add_iff_right : ∀ {m n k : ℕ∞}, k ≠ ⊤ → (n + k < m + k ↔ n < m)
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.uniformContinuous_extension : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β} [CompleteSpace β],
  UniformContinuous (UniformSpace.Completion.extension f)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.mk_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X)
  (snd : W ⟶ Y)
  (eq :
    autoParam (CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g)
      CategoryTheory.Limits.PullbackCone.mk._auto_1)
  (j : CategoryTheory.Limits.WalkingCospan),
  (CategoryTheory.Limits.PullbackCone.mk fst snd eq).π.app j =
    Option.casesOn j (CategoryTheory.CategoryStruct.comp fst f) fun j' =>
      CategoryTheory.Limits.WalkingPair.casesOn j' fst snd
-- Mathlib.Algebra.Algebra.Field
algebraMap.coe_ratCast : ∀ (R : Type u_1) (A : Type u_2) [inst : Field R] [inst_1 : DivisionRing A] [inst_2 : Algebra R A] (q : ℚ), ↑↑q = ↑q
-- Mathlib.Topology.EMetricSpace.Pi
instEDistForall : {β : Type v} → {X : β → Type u_2} → [Fintype β] → [(b : β) → EDist (X b)] → EDist ((b : β) → X b)
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Combinators.Monadic.FlatMap.0.Std.Iterators.Types.Flatten.productiveRel_of_right₂ : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m (Std.IterM m β)]
  [inst_2 : Std.Iterator α₂ m β] [inst_3 : Std.Iterators.Finite α m] [inst_4 : Std.Iterators.Productive α₂ m]
  {it₁ : Std.IterM m (Std.IterM m β)} {it₂ : Std.IterM m β},
  Std.Iterators.Types.Flatten.ProductiveRel✝ α β m { internalState := { it₁ := it₁, it₂ := none } }
    { internalState := { it₁ := it₁, it₂ := some it₂ } }
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.instT2Space : ∀ {A : Type u_1} [inst : Monoid A] [inst_1 : TopologicalSpace A], T2Space (PontryaginDual A)
-- Mathlib.RingTheory.Localization.Module
/-- The `S⁻¹R`-linear isomorphisms between two `S⁻¹R`-modules are exactly the `R`-linear
isomorphisms.  -/
LinearEquiv.extendScalarsOfIsLocalizationEquiv : {R : Type u_3} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      (A : Type u_4) →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [IsLocalization S A] →
              {M : Type u_5} →
                {N : Type u_6} →
                  [inst_4 : AddCommMonoid M] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module A M] →
                        [IsScalarTower R A M] →
                          [inst_8 : AddCommMonoid N] →
                            [inst_9 : Module R N] →
                              [inst_10 : Module A N] → [IsScalarTower R A N] → (M ≃ₗ[R] N) ≃ M ≃ₗ[A] N
-- Mathlib.Data.NNReal.Defs
NNReal.exists_nat_pos_inv_lt : ∀ {b : NNReal}, 0 < b → ∃ n, 0 < n ∧ (↑n)⁻¹ < b
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The equivalence between `AddCommMonCat` and `CommMonCat`.  -/
AddCommMonCat.equivalence : AddCommMonCat ≌ CommMonCat
-- Mathlib.Algebra.Star.Basic
starRingEnd_self_apply : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : StarRing R] (x : R), (starRingEnd R) ((starRingEnd R) x) = x
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_neg : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α)
  (p₁ p₂ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.eq_neg_cert p₁ p₂ = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ = 0 → Lean.Grind.Linarith.Poly.denote' ctx p₂ = 0
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity follows from pairwise scaled distance. Backward direction of
`similar_iff_exists_pairwise_dist_eq`.  -/
Similar.of_exists_pairwise_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  (∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ => dist (v₁ i₁) (v₁ i₂) = ↑r * dist (v₂ i₁) (v₂ i₂)) → Similar v₁ v₂
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.IsMono.eq_1 : ∀ {α : Type u_5} {ι : Type u_6} {κ : Sort u_7} (C : (ι → α) → κ) (l : Combinatorics.Line α ι),
  Combinatorics.Line.IsMono C l = ∃ c, ∀ (x : α), C (↑l x) = c
-- Mathlib.Order.SupClosed
supClosure_prod : ∀ {α : Type u_3} {β : Type u_4} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] (s : Set α) (t : Set β),
  supClosure (s ×ˢ t) = supClosure s ×ˢ supClosure t
-- Mathlib.Logic.Small.Set
small_inter_of_right : ∀ {α : Type u1} (s t : Set α) [Small.{u, u1} ↑t], Small.{u, u1} ↑(s ∩ t)
-- Mathlib.RingTheory.Spectrum.Prime.Defs
PrimeSpectrum.mk.injEq : ∀ {R : Type u_1} [inst : CommSemiring R] (asIdeal : Ideal R) (isPrime : asIdeal.IsPrime) (asIdeal_1 : Ideal R)
  (isPrime_1 : asIdeal_1.IsPrime),
  ({ asIdeal := asIdeal, isPrime := isPrime } = { asIdeal := asIdeal_1, isPrime := isPrime_1 }) = (asIdeal = asIdeal_1)
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.ext_iff : ∀ {α : Type u_1} {n : Type u_4} [inst : Star α] {A : Matrix n n α}, A.IsHermitian ↔ ∀ (i j : n), star (A j i) = A i j
-- Mathlib.Topology.FiberBundle.Trivialization
/-- This structure contains the information left for a local trivialization (which is implemented
below as `Trivialization F proj`) if the total space has not been given a topology, but we
have a topology on both the fiber and the base space. Through the construction
`topological_fiber_prebundle F proj` it will be possible to promote a
`Pretrivialization F proj` to a `Trivialization F proj`.  -/
Bundle.Pretrivialization : {B : Type u_1} →
  (F : Type u_2) → {Z : Type u_4} → [TopologicalSpace B] → [TopologicalSpace F] → (Z → B) → Type (max (max u_1 u_2) u_4)
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
isLocalDiffeomorph_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N},
  IsLocalDiffeomorph I J n f ↔ ∀ (x : M), IsLocalDiffeomorphAt I J n f x
-- Mathlib.Algebra.Torsor.Basic
Prod.mk_smul_mk : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : Group G] [inst_1 : Group G']
  [inst_2 : Torsor G P] [inst_3 : Torsor G' P'] (v : G) (v' : G') (p : P) (p' : P'),
  (v, v') • (p, p') = (v • p, v' • p')
-- Std.Http.Data.Headers
Std.Http.instReprHeaders.repr : Std.Http.Headers → ℕ → Std.Format
-- Mathlib.Logic.Unique
Unique.instSubsingleton : ∀ {α : Sort u_1} [Unique α], Subsingleton α
-- Mathlib.Data.Sym.Basic
/-- This is `cons` but for the alternative `Sym'` definition.
 -/
Sym.«term_::_» : Lean.TrailingParserDescr
-- Mathlib.Order.UpperLower.Closure
subset_lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, s ⊆ ↑(lowerClosure s)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- Make an object in `TopModuleCat R` from an unbundled topological module.  -/
TopModuleCat.of : (R : Type u) →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      (M : Type v) →
        [inst_2 : AddCommGroup M] →
          [inst_3 : Module R M] →
            [inst_4 : TopologicalSpace M] → [ContinuousAdd M] → [ContinuousSMul R M] → TopModuleCat R
-- Mathlib.Topology.Filter
Filter.HasBasis.nhds : ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → (nhds l).HasBasis p fun i => Set.Iic (Filter.principal (s i))
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.gfpApprox_eq_of_fixedPoint_or_zero : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α},
  f x ≤ x → ∀ (o : Ordinal.{u}), OrdinalApprox.gfpApprox f x o = x ↔ f x = x ∨ o = 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t t_1 : Std.DTreeMap.Raw α β cmp) (e_t : t = t_1) (a a_1 : α)
  (e_a : a = a_1) (h : a ∈ t), t.getKey a h = t_1.getKey a_1 ⋯
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForILeans.noConfusionType : Sort v✝ → Lean.Lsp.WaitForILeans → Lean.Lsp.WaitForILeans → Sort v✝
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.tendsto_atTop_r_real : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r) (i : α), Filter.Tendsto (fun n => ↑(r i n)) Filter.atTop Filter.atTop
-- Mathlib.Analysis.Convex.Hull
convexHull_add_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s t : Set E}, (convexHull 𝕜) (s + t) ⊆ (convexHull 𝕜) s + (convexHull 𝕜) t
-- Mathlib.Tactic.DeriveTraversable
/-- Simplify the goal `m` using `functor_norm`.  -/
Mathlib.Deriving.Traversable.simpFunctorGoal : Lean.MVarId →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.SimprocsArray ∅ →
      optParam (Option Lean.Meta.Simp.Discharge) none →
        optParam Bool true →
          optParam (Array Lean.FVarId) #[] →
            optParam Lean.Meta.Simp.Stats { } →
              Lean.MetaM (Option (Array Lean.FVarId × Lean.MVarId) × Lean.Meta.Simp.Stats)