mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.Height
Ideal.exists_isPrime_height_eq : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {n : ℕ},
  I.height = ↑n → ∃ p, ∃ (_ : p.IsPrime) (_ : I ≤ p), p.height = ↑n
-- Std.Do.Triple.Basic
Std.Do.Triple.instPropAsSPredTautologyImpApplyWp : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond α ps}
  [inst : Std.Do.WP m ps] (x : m α),
  Std.Do.SPred.Tactic.PropAsSPredTautology (⦃P⦄ x ⦃Q⦄) spred(P → (Std.Do.wp x).apply Q)
-- Mathlib.Algebra.Quaternion
Quaternion.self_add_star' : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), a + star a = ↑(2 * a.re)
-- Init.Data.Ord.Array
Array.compareLex : {α : Type u_1} → (α → α → Ordering) → Array α → Array α → Ordering
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- Given a short complex `S` such that `S.HasHomology`, this is the canonical
left homology data for `S` whose `K` and `H` fields are
respectively `S.cycles` and `S.homology`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.canonical : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [S.HasHomology] → S.LeftHomologyData
-- Mathlib.FieldTheory.AbelRuffini
IsSolvableByRad.below.mul : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  {motive : (a : E) → IsSolvableByRad F a → Prop} (α β : E) (a : IsSolvableByRad F α) (a_1 : IsSolvableByRad F β),
  IsSolvableByRad.below a → motive α a → IsSolvableByRad.below a_1 → motive β a_1 → IsSolvableByRad.below ⋯
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.map_prod_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {δ : Type u_4} [inst_3 : MeasurableSpace δ] {f : α → β} {g : γ → δ}
  (μa : MeasureTheory.Measure α) (μc : MeasureTheory.Measure γ) [MeasureTheory.SFinite μa] [MeasureTheory.SFinite μc],
  Measurable f →
    Measurable g →
      (MeasureTheory.Measure.map f μa).prod (MeasureTheory.Measure.map g μc) =
        MeasureTheory.Measure.map (Prod.map f g) (μa.prod μc)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumInr_onFunction : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ℕ) (val : L'.Functions _n),
  FirstOrder.Language.LHom.sumInr.onFunction val = Sum.inr val
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.vertexSet_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, G.vertexSet = ∅ ↔ G = ⊥
-- Aesop.Forward.State
/-- Find matches in slot `slot - 1` whose substitutions are compatible with
`subst`. Preconditions: `slot.index` is nonzero, `slot.common` is nonempty and
each variable contained in `slot.common` is also contained in `subst`.  -/
Aesop.VariableMap.findMatches : Aesop.VariableMap → Aesop.Slot → Aesop.Substitution → Aesop.BaseM (Std.HashSet Aesop.Match)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceLeDiff : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.Order.IsLUB
IsLUB.isGLB_of_tendsto : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : Preorder γ] [inst_4 : TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ},
  AntitoneOn f s → IsLUB s a → s.Nonempty → Filter.Tendsto f (nhdsWithin a s) (nhds b) → IsGLB (f '' s) b
-- Mathlib.Order.Cofinal
/-- In a linear order with no maximum, cofinal sets are the same as unbounded sets.  -/
not_isCofinal_iff_bddAbove : ∀ {α : Type u_1} [inst : LinearOrder α] [NoMaxOrder α] {s : Set α}, ¬IsCofinal s ↔ BddAbove s
-- Mathlib.Algebra.Group.Finsupp
Finsupp.addCommute_of_disjoint : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] {f g : ι →₀ M}, Disjoint f.support g.support → AddCommute f g
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- `Matrix.vecMul M` is a linear map.

Note this is a special case of `Matrix.vecMulBilin`.  -/
Matrix.vecMulLinear : {R : Type u_1} →
  [inst : Semiring R] → {m : Type u_3} → {n : Type u_4} → [Fintype m] → Matrix m n R → (m → R) →ₗ[R] n → R
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- **Alias** of `ClosedSubmodule.mem_orthogonal_toSubmodule_iff`. -/
ClosedSubmodule.mem_orthogonal_iff : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : ClosedSubmodule 𝕜 E) (v : E), v ∈ (↑K)ᗮ ↔ v ∈ Kᗮ
-- Mathlib.Order.Category.DistLat
DistLat.ext : ∀ {X Y : DistLat} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.continuous_mk_symm : ∀ {M : Type u_1} [inst : TopologicalSpace M], Continuous ⇑DomMulAct.mk.symm
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_neg_one : ∀ (x : ℂ), x ^ (-1) = x⁻¹
-- Std.Http.Data.Headers
/-- Merges two headers, accumulating values for duplicate keys from both.
 -/
Std.Http.Headers.merge : Std.Http.Headers → Std.Http.Headers → Std.Http.Headers
-- Batteries.Data.Array.Match
Array.Matcher.modifyStep.eq_3 : ∀ {α σ : Type u_1} {n : Type u_1 → Type u_2} [inst : BEq α] (m : Array.Matcher α) [inst_1 : Std.Iterator σ n α]
  (it : Std.IterM n σ) (it' : Std.IterM n α) (x_1 : α)
  (property : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' x_1)),
  m.modifyStep it ⟨Std.IterStep.yield it' x_1, property⟩ =
    if ↑(m.table.step x_1 m.state) = m.table.size then
      Std.IterStep.yield { internalState := { inner := it', state := m.table.step x_1 m.state } } it'.internalState
    else Std.IterStep.skip { internalState := { inner := it', state := m.table.step x_1 m.state } }
-- Mathlib.CategoryTheory.Action.Limits
/-- `F : C ⥤ Action V G` preserves the limit of some `K : J ⥤ C` if
it does after postcomposing with the forgetful functor `Action V G ⥤ V`.  -/
Action.preservesLimit_of_preserves : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} C] (F : CategoryTheory.Functor C (Action V G)) {J : Type u_4}
  [inst_3 : CategoryTheory.Category.{v_3, u_4} J] (K : CategoryTheory.Functor J C),
  CategoryTheory.Limits.PreservesLimit K (F.comp (Action.forget V G)) → CategoryTheory.Limits.PreservesLimit K F
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableSub₂.mk : ∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Sub G], (Measurable fun p => p.1 - p.2) → MeasurableSub₂ G
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (e : M ≃ₜ+ N), Function.Surjective ⇑e
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.entails_4 : ∀ {σ₁ σ₂ σ₃ σ₄ : Type u_1} {P Q : Std.Do.SPred [σ₁, σ₂, σ₃, σ₄]},
  P ⊢ₛ Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄), (P s₁ s₂ s₃ s₄).down → (Q s₁ s₂ s₃ s₄).down
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- Given a continuous function `g : β → γ`, and an almost everywhere equal function `[f] : α →ₘ β`,
return the equivalence class of `g ∘ f`, i.e., the almost everywhere equal function
`[g ∘ f] : α →ₘ γ`.  -/
MeasureTheory.AEEqFun.comp : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : TopologicalSpace γ] → (g : β → γ) → Continuous g → (α →ₘ[μ] β) → α →ₘ[μ] γ
-- Mathlib.LinearAlgebra.Alternating.Basic
LinearMap.subtype_compAlternatingMap_codRestrict : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N)
  (h : ∀ (v : ι → M), f v ∈ p), p.subtype.compAlternatingMap (f.codRestrict p h) = f
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- This is an `IsLocalization.AtPrime` version for `IsLocalization.isDomain_of_local_atPrime`.  -/
IsLocalization.isDomain_of_atPrime : ∀ {A : Type u_4} [inst : CommRing A] [IsDomain A] (S : Type u_5) [inst_2 : CommSemiring S] [inst_3 : Algebra A S]
  (P : Ideal A) [inst_4 : P.IsPrime] [IsLocalization.AtPrime S P], IsDomain S
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.of_eq : ∀ {f g : ℕ → ℕ}, Nat.Primrec f → (∀ (n : ℕ), f n = g n) → Nat.Primrec g
-- Mathlib.Algebra.Category.Ring.Adjunctions
/-- The free-forgetful adjunction for commutative rings.  -/
CommRingCat.adj : CommRingCat.free ⊣ CategoryTheory.forget CommRingCat
-- Mathlib.Algebra.Star.Pointwise
Set.star_subset_star : ∀ {α : Type u_1} [inst : InvolutiveStar α] {s t : Set α}, star s ⊆ star t ↔ s ⊆ t
-- Mathlib.Order.Hom.Bounded
TopHom.dual_apply_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : OrderTop α] [inst_2 : LE β] [inst_3 : OrderTop β]
  (f : TopHom α β) (a : α), (TopHom.dual f) a = f a
-- Mathlib.Algebra.Order.Group.Defs
LinearOrderedCommGroup.to_noMinOrder : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] [Nontrivial α], NoMinOrder α
-- Mathlib.Order.WithBot
/-- The order on `WithBot α`, defined by `⊥ < ↑a` and `a < b → ↑a < ↑b`.

Equivalently, `x < y` can be defined as `∃ b : α, y = ↑b ∧ ∀ a : α, x = ↑a → a < b`,
see `lt_iff_exists`. The definition as an inductive predicate is preferred since it
cannot be accidentally unfolded too far.  -/
WithBot.instLT : {α : Type u_1} → [LT α] → LT (WithBot α)
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.create.sizeOf_spec : ∀ (a : Lean.Lsp.CreateFile), sizeOf (Lean.Lsp.DocumentChange.create a) = 1 + sizeOf a
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
/-- `RightPreLieRing`s are `NonUnitalNonAssocRing`s such that the `associator` is symmetric in the
last two variables.  -/
RightPreLieRing : Type u_1 → Type u_1
-- Aesop.RuleSet
Aesop.GlobalRuleSet.empty : Aesop.GlobalRuleSet
-- Init.Data.Int.Order
Int.lt_sub_right_of_add_lt : ∀ {a b c : ℤ}, a + b < c → a < c - b
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (f : α →𝒄 β), OmegaCompletePartialOrder.ωScottContinuous ⇑f
-- Mathlib.Topology.MetricSpace.Perfect
_private.Mathlib.Topology.MetricSpace.Perfect.0.Perfect.small_diam_aux : ∀ {α : Type u_1} [inst : MetricSpace α] {C : Set α} {ε : ENNReal},
  Perfect C →
    0 < ε →
      ∀ {x : α},
        x ∈ C →
          have D := closure (Metric.eball x (ε / 2) ∩ C);
          Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ Metric.ediam D ≤ ε
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_succ_Ico_succ : ∀ {n : ℕ} (i j : Fin n), Fin.succ ⁻¹' Set.Ico i.succ j.succ = Set.Ico i j
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addZ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (P Q : Fin 3 → R), WeierstrassCurve.Jacobian.addZ P Q = P 0 * Q 2 ^ 2 - Q 0 * P 2 ^ 2
-- Mathlib.MeasureTheory.Measure.Support
Filter.HasBasis.mem_measureSupport : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : Sort u_2}
  {p : ι → Prop} {s : ι → Set X} {x : X}, (nhds x).HasBasis p s → (x ∈ μ.support ↔ ∀ (i : ι), p i → 0 < μ (s i))
-- Mathlib.CategoryTheory.ComposableArrows.Basic
Fin.castSuccFunctor_obj : ∀ (n : ℕ) (i : Fin n), (Fin.castSuccFunctor n).obj i = i.castSucc
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.differential.congr_simp : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_3 : Finite σ], P.differential = P.differential
-- Mathlib.Algebra.Group.Hom.Basic
/-- Makes an additive group homomorphism from a proof that the map preserves
the operation `fun a b => a + -b`. See also `AddMonoidHom.ofMapSub` for a version using
`fun a b => a - b`.  -/
AddMonoidHom.ofMapAddNeg : {G : Type u_5} →
  [inst : AddGroup G] →
    {H : Type u_8} → [inst_1 : AddGroup H] → (f : G → H) → (∀ (a b : G), f (a + -b) = f a + -f b) → G →+ H
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.inv_η : ∀ {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 : F.Monoidal],
  CategoryTheory.inv (CategoryTheory.Functor.OplaxMonoidal.η F) = CategoryTheory.Functor.LaxMonoidal.ε F
-- Init.Data.Subtype.Order
Subtype.instMin : {α : Type u} → [inst : Min α] → [Std.MinEqOr α] → {P : α → Prop} → Min (Subtype P)
-- Lean.Widget.InteractiveCode
Lean.Widget.DiffTag.noConfusionType : Sort v✝ → Lean.Widget.DiffTag → Lean.Widget.DiffTag → Sort v✝
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
min_add_add_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Add α] [AddRightMono α] (a b c : α), min (a + c) (b + c) = min a b + c
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkMap_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↥X),
  AlgebraicGeometry.Scheme.Hom.stalkMap (CategoryTheory.CategoryStruct.comp f g) x =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap g (f x))
      (AlgebraicGeometry.Scheme.Hom.stalkMap f x)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {Y : C} {T : CategoryTheory.Functor C D} {f : S' ⟶ T.obj Y} (g : S ⟶ S'),
  (CategoryTheory.StructuredArrow.map g).obj (CategoryTheory.StructuredArrow.mk f) =
    CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.Logic.Equiv.Defs
Equiv.coe_ofBijective : ∀ {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f), ⇑(Equiv.ofBijective f hf) = f
-- Mathlib.Data.Finite.Prod
Finite.prod_left : ∀ {α : Type u_1} (β : Type u_3) [Finite (α × β)] [Nonempty β], Finite α
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.instHasNoLoopNatDown : (ComplexShape.down ℕ).HasNoLoop
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
SimpleGraph.odd_ncard_oddComponents : ∀ {V : Type u} (G : SimpleGraph V) [Finite V], Odd G.oddComponents.ncard ↔ Odd (Nat.card V)
-- Init.Data.Array.Subarray
Std.Slice.Internal.SubarrayData.mk : {α : Type u} →
  (array : Array α) → (start stop : ℕ) → start ≤ stop → stop ≤ array.size → Std.Slice.Internal.SubarrayData α
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.isReal_conjugate_iff : ∀ {K : Type u_1} [inst : Field K] {φ : K →+* ℂ},
  NumberField.ComplexEmbedding.IsReal (NumberField.ComplexEmbedding.conjugate φ) ↔ NumberField.ComplexEmbedding.IsReal φ
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.corec_unique : ∀ {P : PFunctor.{uA, uB}} {α : Type u_2} (g : α → ↑P α) (f : α → P.M),
  (∀ (x : α), (f x).dest = P.map f (g x)) → f = PFunctor.M.corec g
-- Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
_private.Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp.0.«term_~ᵤ_» : Lean.TrailingParserDescr
-- Std.Data.DHashMap.RawDef
/-- Checks if any element satisfies the predicate, short-circuiting if a predicate succeeds.  -/
Std.DHashMap.Raw.any : {α : Type u} → {β : α → Type v} → Std.DHashMap.Raw α β → ((a : α) → β a → Bool) → Bool
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.lift_comp_ι : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (g : TensorAlgebra R M →ₐ[R] A),
  (TensorAlgebra.lift R) (g.toLinearMap ∘ₗ TensorAlgebra.ι R) = g
-- Mathlib.RingTheory.Localization.Away.Basic
Module.eqIdeal.eq_1 : ∀ (R : Type u_1) {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m m' : M),
  Module.eqIdeal R m m' = { carrier := {r | r • m = r • m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : Std.Tactic.BVDecide.LRAT.Action β α → Sort u_3) (id : ℕ) (c : β)
  (p : Std.Sat.Literal α) (rupHints : Array ℕ) (ratHints : Array (ℕ × Array ℕ))
  (h_1 :
    (id : ℕ) →
      (c : β) →
        (p : Std.Sat.Literal α) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) → motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c p rupHints ratHints))
  (h_2 : (x : Std.Tactic.BVDecide.LRAT.Action β α) → motive x),
  (match Std.Tactic.BVDecide.LRAT.Action.addRat id c p rupHints ratHints with
    | Std.Tactic.BVDecide.LRAT.Action.addRat id c p rupHints ratHints => h_1 id c p rupHints ratHints
    | x => h_2 x) =
    h_1 id c p rupHints ratHints
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.instMonoid : {A : Type u_1} → [inst : NonUnitalNonAssocSemiring A] → [inst_1 : Star A] → Monoid (A →⋆ₙ+* A)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R),
  CategoryTheory.CategoryStruct.comp (K.ι (J.fst b)) (I.fst b) =
    CategoryTheory.CategoryStruct.comp (K.ι (J.snd b)) (I.snd b)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.hasBinaryProducts_of_hasBinaryBiproducts : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasBinaryBiproducts C], CategoryTheory.Limits.HasBinaryProducts C
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_filter_key_iff : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {f : α → Bool},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filter (fun a x => f a) m)).isEmpty = true ↔
      ∀ (k : α) (h : m.contains k = true), f (m.getKey k h) = false)
-- Mathlib.Combinatorics.Matroid.Constructions
/-- The `Matroid α` with ground set `E` whose only base is `∅`.
The elements are all 'loops' - see `Matroid.IsLoop` and `Matroid.loopyOn_isLoop_iff`.  -/
Matroid.loopyOn : {α : Type u_1} → Set α → Matroid α
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.withTopOrderIso_symm_apply : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a : M} (h : a ≠ 1),
  (FiniteMulArchimedeanClass.withTopOrderIso M).symm (MulArchimedeanClass.mk a) = ↑(FiniteMulArchimedeanClass.mk a h)
-- Mathlib.Analysis.Normed.Operator.Banach
LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [inst_7 : RingHomIsometric σ] [inst_8 : RingHomIsometric σ'] [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E]
  [inst_11 : RingHomInvPair σ' σ] (e : E ≃ₛₗ[σ] F) (h : Continuous ⇑e), ⇑(e.toContinuousLinearEquivOfContinuous h) = ⇑e
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- The inclusion map from the sum of `GoodProducts (π C (ord I · < o))` and
`(MaxProducts C ho)` to `Products I`.  -/
Profinite.NobelingProof.GoodProducts.sum_to : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        {o : Ordinal.{u}} →
          (ho : o < Ordinal.type fun x1 x2 => x1 < x2) →
            ↑(Profinite.NobelingProof.GoodProducts
                    (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)) ⊕
                ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho) →
              Profinite.NobelingProof.Products I
-- Mathlib.Analysis.LocallyConvex.Basic
absorbent_iff_eventually_nhdsNE_zero : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E}, Absorbent 𝕜 s ↔ ∀ (x : E), ∀ᶠ (c : 𝕜) in nhdsWithin 0 {0}ᶜ, c • x ∈ s
-- Mathlib.Topology.SmallInductiveDimension
/-- For a topological space, the property of having small inductive dimension less than `n : ℕ`  is
inductively defined as follows. Empty spaces have small inductive dimension less than 0, and a
topological space has dimension less than `n + 1` if it has a topological basis whose elements have
frontiers of dimension strictly less `n`.
 -/
HasSmallInductiveDimensionLT : (X : Type u) → [TopologicalSpace X] → ℕ → Prop
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `FunLike.coeAddMonoidHom`. -/
MeasureTheory.VectorMeasure.coeFnAddMonoidHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) →
      [inst : FunLike F α β] →
        [inst_1 : AddZero F] → [inst_2 : AddZeroClass β] → [IsZeroApply F α β] → [IsAddApply F α β] → F →+ α → β
-- Init.Data.Slice.Array.Lemmas
Subarray.toList_mkSlice_rio : ∀ {α : Type u_1} {xs : Subarray α} {hi : ℕ},
  Std.Slice.toList (Std.Rio.Sliceable.mkSlice xs *...hi) = List.take hi (Std.Slice.toList xs)
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_leftInverse : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f : σ → τ} {g : τ → σ},
  Function.LeftInverse f g → Function.LeftInverse ⇑(MvPolynomial.rename f) ⇑(MvPolynomial.rename g)
-- Mathlib.Data.Multiset.MapFold
Multiset.map_mk_eq_map_mk_of_rel : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Multiset α},
  Multiset.Rel r s t → Multiset.map (Quot.mk r) s = Multiset.map (Quot.mk r) t
-- Mathlib.Analysis.Normed.Group.Bounded
NormedAddCommGroup.cauchySeq_iff : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedAddGroup E] [Nonempty α] [inst_2 : SemilatticeSup α] {u : α → E},
  CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖-u m + u n‖ < ε
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {fallback : α}, t.getD t.max! fallback = t.max!
-- Mathlib.Algebra.Group.Submonoid.Defs
SubmonoidClass.toOneMemClass : ∀ {S : Type u_3} {M : outParam (Type u_4)} {inst : MulOneClass M} {inst_1 : SetLike S M} [self : SubmonoidClass S M],
  OneMemClass S M
-- Mathlib.Algebra.Order.Ring.Abs
pow_eq_one_iff_cases : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ},
  a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The spectral norm is a multiplicative `K`-algebra norm on `L`.  -/
spectralMulAlgNorm : (K : Type u) →
  [inst : NontriviallyNormedField K] →
    (L : Type v) →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [Algebra.IsAlgebraic K L] → [hu : IsUltrametricDist K] → [CompleteSpace K] → MulAlgebraNorm K L
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovaryOn_inv₀`. -/
MonovaryOn.of_inv₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Semifield β] [inst_4 : LinearOrder β] [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < f i) → (∀ i ∈ s, 0 < g i) → MonovaryOn f⁻¹ g⁻¹ s → MonovaryOn f g s
-- Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
HomotopicalAlgebra.leftHomotopyClassToHom.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {H : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H)
  [inst_3 : L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] {X Y : C}
  (a a_1 : HomotopicalAlgebra.LeftHomotopyClass X Y),
  a = a_1 → HomotopicalAlgebra.leftHomotopyClassToHom L a = HomotopicalAlgebra.leftHomotopyClassToHom L a_1