mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.ω₁δ.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b c : EInt) (hab : a ≤ b)
  (hbc : b ≤ c), t.ω₁δ a b c hab hbc = t.ω₁δ a b c hab hbc
-- Mathlib.Data.ENNReal.Basic
ENNReal.lt_iff_exists_real_btwn : ∀ {a b : ENNReal}, a < b ↔ ∃ r, 0 ≤ r ∧ a < ENNReal.ofReal r ∧ ENNReal.ofReal r < b
-- Mathlib.Data.List.AList
List.toAList.eq_1 : ∀ {α : Type u} [inst : DecidableEq α] {β : α → Type v} (l : List (Sigma β)),
  l.toAList = { entries := l.dedupKeys, nodupKeys := ⋯ }
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- If `s` is a countable family of compact sets covering `X`, `f` is a continuous function, and
the sequence `‖f.restrict (s i)‖ * μ (s i)` is summable, then `f` is integrable.  -/
MeasureTheory.integrable_of_summable_norm_restrict : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} {ι : Type u_5} [Countable ι] {μ : MeasureTheory.Measure X}
  [inst : NormedAddCommGroup E] [inst_1 : TopologicalSpace X] [BorelSpace X] [T2Space X]
  [MeasureTheory.IsLocallyFiniteMeasure μ] {f : C(X, E)} {s : ι → TopologicalSpace.Compacts X},
  (Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * μ.real ↑(s i)) →
    ⋃ i, ↑(s i) = Set.univ → MeasureTheory.Integrable (⇑f) μ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k ↑B ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((groupCohomology.cochainsMap f φ).f 0)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₀ B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₀ A).hom
      (CategoryTheory.CategoryStruct.comp (Rep.Hom.toModuleCatHom φ) h)
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.typevec_proc : Lean.ParserDescr
-- Mathlib.RingTheory.RingHom.Locally
/-- If `P` is stable under composition with localization away maps on the right,
then so is `Locally P`.  -/
RingHom.locally_stableUnderCompositionWithLocalizationAwayTarget : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P) →
    RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] =>
      RingHom.Locally fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.nnnorm_eq_zero_iff : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : ↥(MeasureTheory.Lp E p μ)}, 0 < p → (‖f‖₊ = 0 ↔ f = 0)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.cokernelSequence_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.ShortComplex.cokernelSequence f).f = f
-- Lean.Parser.StrInterpolation
/-- The parser `interpolatedStr(p)` parses a string literal like `"foo"` (see `str`), but the string
may also contain `{}` escapes, and within the escapes the parser `p` is used. For example,
`interpolatedStr(term)` will parse `"foo {2 + 2}"`, where `2 + 2` is parsed as a term rather than
as a string. Note that the full Lean term grammar is available here, including string literals,
so for example `"foo {"bar" ++ "baz"}"` is a legal interpolated string (which evaluates to
`foo barbaz`).

This parser has arity 1, and returns a `interpolatedStrKind` with an odd number of arguments,
alternating between chunks of literal text and results from `p`. The literal chunks contain
uninterpreted substrings of the input. For example, `"foo\n{2 + 2}"` would have three arguments:
an atom `"foo\n{`, the parsed `2 + 2` term, and then the atom `}"`.  -/
Lean.Parser.interpolatedStr : Lean.Parser.Parser → Lean.Parser.Parser
-- Lean.Meta.Coe
/-- Coerces `expr` to the type `expectedType`.
Returns `.some coerced` on successful coercion,
`.none` if the expression cannot by coerced to that type,
or `.undef` if we need more metavariable assignments.
 -/
Lean.Meta.coerce? : Lean.Expr → Lean.Expr → Lean.MetaM (Lean.LOption Lean.Expr)
-- Mathlib.Analysis.Calculus.LHopital
/-- L'Hôpital's rule for approaching a real, `HasDerivAt` version. This
does not require anything about the situation at `a`  -/
HasDerivAt.lhopital_zero_nhdsNE : ∀ {a : ℝ} {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in nhdsWithin a {a}ᶜ, HasDerivAt f (f' x) x) →
    (∀ᶠ (x : ℝ) in nhdsWithin a {a}ᶜ, HasDerivAt g (g' x) x) →
      (∀ᶠ (x : ℝ) in nhdsWithin a {a}ᶜ, g' x ≠ 0) →
        Filter.Tendsto f (nhdsWithin a {a}ᶜ) (nhds 0) →
          Filter.Tendsto g (nhdsWithin a {a}ᶜ) (nhds 0) →
            Filter.Tendsto (fun x => f' x / g' x) (nhdsWithin a {a}ᶜ) l →
              Filter.Tendsto (fun x => f x / g x) (nhdsWithin a {a}ᶜ) l
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.RelevantArg.arg.injEq : ∀ (n n_1 : ℕ), (Mathlib.Tactic.Translate.RelevantArg.arg n = Mathlib.Tactic.Translate.RelevantArg.arg n_1) = (n = n_1)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_insertMany_list_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List (α × β)}, (t.insertMany l).size ≤ t.size + l.length
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_alter_of_compare_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β}, cmp k k' = Ordering.eq → (k' ∈ t.alter k f ↔ (f t[k]?).isSome = true)
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.map_comp : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : C(X, Y)} {A : DiscreteQuotient X} {B : DiscreteQuotient Y} {g : C(Y, Z)}
  {C : DiscreteQuotient Z} (h1 : DiscreteQuotient.LEComap g B C) (h2 : DiscreteQuotient.LEComap f A B),
  DiscreteQuotient.map (g.comp f) ⋯ = DiscreteQuotient.map g h1 ∘ DiscreteQuotient.map f h2
-- Lean.Elab.Tactic.Omega.Core
/-- Construct the proof term associated to a `combo` step.  -/
Lean.Elab.Tactic.Omega.Justification.comboProof : Lean.Omega.Constraint →
  Lean.Omega.Constraint → ℤ → Lean.Omega.Coeffs → ℤ → Lean.Omega.Coeffs → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.full : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] (F : C → D),
  (CategoryTheory.inducedFunctor F).Full
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.language_reverse : ∀ {T : Type u_1} {g : ContextFreeGrammar T}, g.reverse.language = g.language.reverse
-- Mathlib.Data.List.Infix
List.infix_antisymm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₂ <:+: l₁ → l₁ = l₂
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_lt_sub_iff_right : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α} (c : α), a - c < b - c ↔ a < b
-- Lean.Elab.Term.TermElabM
/-- When reporting unexpected universe level metavariables, it is useful to localize the errors
to particular terms, especially at `let` bindings and function binders,
where universe polymorphism is not permitted.
 -/
Lean.Elab.Term.LevelMVarErrorInfo : Type
-- Std.Time.Time.PlainTime
Std.Time.instDecidableEqPlainTime.decEq : (x x_1 : Std.Time.PlainTime) → Decidable (x = x_1)
-- Mathlib.RingTheory.FinitePresentation
/-- If `A` is an `R`-algebra and `S` is an `A`-algebra, both finitely presented, then `S` is
finitely presented as `R`-algebra.  -/
Algebra.FinitePresentation.trans : ∀ (R : Type w₁) (A : Type w₂) (B : Type w₃) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B]
  [Algebra.FinitePresentation R A] [Algebra.FinitePresentation A B], Algebra.FinitePresentation R B
-- Mathlib.FieldTheory.Galois.Abelian
IsAbelianGalois.of_algHom : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Field M] [inst_4 : Algebra K M] (f : L →ₐ[K] M) [IsAbelianGalois K M], IsAbelianGalois K L
-- Aesop.Forward.State
_private.Aesop.Forward.State.0.Aesop.ForwardState.addForwardRuleMatches : Array Aesop.ForwardRuleMatch → Aesop.ForwardRule → Array Aesop.CompleteMatch → Lean.MetaM (Array Aesop.ForwardRuleMatch)
-- Mathlib.GroupTheory.Torsion
AddCommGroup.torsion_eq_top_iff : ∀ {G : Type u_1} [inst : AddCommGroup G], AddCommGroup.torsion G = ⊤ ↔ IsAddTorsion G
-- Lean.Parser.Command
Lean.Parser.Command.declId.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `none` if the
map is empty.
 -/
Std.TreeMap.maxEntry? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Option (α × β)
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `E` and `K` are field extensions of `F`, one of them is algebraic, such that
`E ⊗[F] K` is a domain, then `E ⊗[F] K` is also a field. It is a corollary of
`Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective` and
`IntermediateField.sup_toSubalgebra_of_isAlgebraic`.
See `Algebra.TensorProduct.isAlgebraic_of_isField` for its converse (in an earlier file).  -/
Algebra.TensorProduct.isField_of_isAlgebraic : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type u_1) [inst_3 : Field K]
  [inst_4 : Algebra F K] [IsDomain (TensorProduct F E K)],
  Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F K → IsField (TensorProduct F E K)
-- Mathlib.Algebra.Field.Rat
Rat.div_nonneg : ∀ {a b : ℚ}, 0 ≤ a → 0 ≤ b → 0 ≤ a / b
-- Mathlib.SetTheory.Ordinal.Notation
NONote.repr_sub : ∀ (a b : NONote), (a - b).repr = a.repr - b.repr
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion at `x`, then it is the uniform limit of the
partial sums of this power series on strict subdisks of the disk of convergence, i.e., `f y`
is the uniform limit of `p.partialSum n (y - x)` there.  -/
HasFPowerSeriesOnBall.tendstoUniformlyOn' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : NNReal},
  HasFPowerSeriesOnBall f p x r →
    ↑r' < r → TendstoUniformlyOn (fun n y => p.partialSum n (y - x)) f Filter.atTop (Metric.ball x ↑r')
-- Mathlib.CategoryTheory.Action.Limits
CategoryTheory.Functor.mapAction_preadditive : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_2, u_3} W] (F : CategoryTheory.Functor V W) (G : Type u_4) [inst_2 : Monoid G]
  [inst_3 : CategoryTheory.Preadditive V] [inst_4 : CategoryTheory.Preadditive W] [F.Additive], (F.mapAction G).Additive
-- Mathlib.Algebra.Order.Hom.Basic
SubadditiveHomClass.mk : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : Add α] [inst_1 : Add β] [inst_2 : LE β]
  [inst_3 : FunLike F α β], (∀ (f : F) (a b : α), f (a + b) ≤ f a + f b) → SubadditiveHomClass F α β
-- Mathlib.GroupTheory.Index
Subgroup.finiteIndex_iInf' : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_3} {s : Finset ι} (f : ι → Subgroup G),
  (∀ i ∈ s, (f i).FiniteIndex) → (⨅ i ∈ s, f i).FiniteIndex
-- Init.Prelude
OrOp.mk : {α : Type u} → (α → α → α) → OrOp α
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.antilipschitz_antiLipschitzConstant_of_injective_of_isClosed_range : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_5} {F : Type u_6} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : CompleteSpace E]
  [inst_6 : CompleteSpace F] (f : E →L[𝕜] F) (hf : Function.Injective ⇑f) (hf' : IsClosed (Set.range ⇑f)),
  AntilipschitzWith (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') ⇑f
-- Mathlib.CategoryTheory.Localization.Trifunctor
CategoryTheory.Localization.lift₃NatTrans_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃]
  [inst_6 : CategoryTheory.Category.{v_13, u_13} E] (L₁ : CategoryTheory.Functor C₁ D₁)
  (L₂ : CategoryTheory.Functor C₂ D₂) (L₃ : CategoryTheory.Functor C₃ D₃) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) (W₃ : CategoryTheory.MorphismProperty C₃) [inst_7 : L₁.IsLocalization W₁]
  [inst_8 : L₂.IsLocalization W₂] [inst_9 : L₃.IsLocalization W₃] [inst_10 : W₁.ContainsIdentities]
  [inst_11 : W₂.ContainsIdentities] [inst_12 : W₃.ContainsIdentities]
  (F₁ F₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)))
  (F₁' F₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E)))
  [inst_13 : CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁']
  [inst_14 : CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'] (τ : F₁ ⟶ F₂) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
  (((CategoryTheory.Localization.lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)).app (L₂.obj X₂)).app
      (L₃.obj X₃) =
    CategoryTheory.CategoryStruct.comp
      ((((CategoryTheory.Localization.Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁').hom.app X₁).app X₂).app X₃)
      (CategoryTheory.CategoryStruct.comp (((τ.app X₁).app X₂).app X₃)
        ((((CategoryTheory.Localization.Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂').inv.app X₁).app X₂).app X₃))
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.preimage_image_of_isIso : ∀ {X Y : SSet} (f : X ⟶ Y) (B : Y.Subcomplex) [CategoryTheory.IsIso f], (B.preimage f).image f = B
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.comap_covBy_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂},
  Function.Surjective ⇑f → ∀ {p q : Submodule R₂ M₂}, p ⋖ q → Submodule.comap f p ⋖ Submodule.comap f q
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
/-- The composition of two pullback functors on presheaves of modules identifies
to the pullback for the composition.  -/
PresheafOfModules.pullbackComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {F : CategoryTheory.Functor C D} →
              {R : CategoryTheory.Functor Dᵒᵖ RingCat} →
                {S : CategoryTheory.Functor Cᵒᵖ RingCat} →
                  (φ : S ⟶ F.op.comp R) →
                    {G : CategoryTheory.Functor D E} →
                      {T : CategoryTheory.Functor Eᵒᵖ RingCat} →
                        (ψ : R ⟶ G.op.comp T) →
                          [inst_3 : (PresheafOfModules.pushforward φ).IsRightAdjoint] →
                            [inst_4 : (PresheafOfModules.pushforward ψ).IsRightAdjoint] →
                              (PresheafOfModules.pullback φ).comp (PresheafOfModules.pullback ψ) ≅
                                PresheafOfModules.pullback (CategoryTheory.CategoryStruct.comp φ (F.op.whiskerLeft ψ))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (t.erase k).size = if t.contains k = true then t.size - 1 else t.size
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionL_add_projectionL_eq_self : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [inst_4 : ContinuousSub M] (h : Submodule.IsTopCompl p q) (x : M),
  (p.projectionL q h) x + (q.projectionL p ⋯) x = x
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.Linear.RingEqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof → Sort u} →
    (t : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof) →
      ((t : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) → t.below → motive_1 t) →
        ((t : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof) → t.below → motive_2 t) → motive_2 t ×' t.below
-- Mathlib.Analysis.CStarAlgebra.ContinuousMap
ZeroAtInftyContinuousMap.instNonUnitalCStarAlgebra : {α : Type u_1} →
  {A : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : NonUnitalCStarAlgebra A] → NonUnitalCStarAlgebra (ZeroAtInftyContinuousMap α A)
-- Mathlib.Data.Multiset.MapFold
Multiset.map_surjective_of_surjective : ∀ {α : Type u_1} {β : Type v} {f : α → β}, Function.Surjective f → Function.Surjective (Multiset.map f)
-- Mathlib.Topology.Compactness.LocallyCompact
IsOpenQuotientMap.locallyCompactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyCompactSpace X]
  {f : X → Y}, IsOpenQuotientMap f → LocallyCompactSpace Y
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toRingEquiv_symm : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (e : A ≃⋆ₐ[R] B),
  (↑e).symm.toRingEquiv = (↑e).symm
-- Mathlib.Order.SuccPred.Archimedean
exists_succ_iterate_or : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {a b : α},
  (∃ n, Order.succ^[n] a = b) ∨ ∃ n, Order.succ^[n] b = a
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
Mathlib.Tactic.ClickSuggestions.ApplyAtLemma.mk : Mathlib.Tactic.ClickSuggestions.Premise → Mathlib.Tactic.ClickSuggestions.ApplyAtLemma
-- Qq.MetaM
/-- The result of `Qq.isLevelDefEqQ`; `MaybeLevelDefEq u v` is an optional version of `$u =QL $v`.  -/
Qq.MaybeLevelDefEq : Lean.Level → Lean.Level → Type
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.fromLocalizedModule'.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f f_1 : M →ₗ[R] M') (e_f : f = f_1)
  [inst_5 : IsLocalizedModule S f] (a a_1 : LocalizedModule S M),
  a = a_1 → IsLocalizedModule.fromLocalizedModule' S f a = IsLocalizedModule.fromLocalizedModule' S f_1 a_1
-- Mathlib.Algebra.Ring.Aut
/-- Monoid homomorphism from ring automorphisms to permutations.  -/
RingAut.toPerm : (R : Type u_1) → [inst : Mul R] → [inst_1 : Add R] → RingAut R →* Equiv.Perm R
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Returns the entry `a` such that `a ≥ k` for all keys in the RBSet.  -/
RBTree.RBSet.max? : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → Option α
-- Init.Data.List.MinMaxIdx
List.maxIdxOn?_eq_if : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α},
  List.maxIdxOn? f xs = if h : xs ≠ [] then some (List.maxIdxOn f xs h) else none
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.inv_anti_mono : ∀ {K : Type u_3} [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {I J : FractionalIdeal (nonZeroDivisors R₁) K}, I ≠ 0 → J ≠ 0 → I ≤ J → J⁻¹ ≤ I⁻¹
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.colimitAddZeroClass : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J AddMonCat) →
      [CategoryTheory.IsFiltered J] → AddZeroClass (AddMonCat.FilteredColimits.M F)
-- Init.Data.BitVec.Lemmas
/-- Accessing bits in `x.rotateRight r` the range `[w-r, w)` is equal to
accessing bits `x` in the range `[0, r)`.

Proof by example:
Let x := <6 5 4 3 2 1 0> : BitVec 7.
x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2>

(x.rotateLeft 2).getLsbD ⟨i, i ≥ 7 - 2⟩
= <1 0 | 6 5 4 3 2>.getLsbD ⟨i, i ≤ 7 - 2⟩
= <1 0>.getLsbD (i - len(<6 5 4 3 2>)
= <6 5 4 3 2 | 1 0> (i - len<6 4 4 3 2>)
  -/
BitVec.getLsbD_rotateRightAux_of_ge : ∀ {w : ℕ} {x : BitVec w} {r i : ℕ},
  i ≥ w - r → (x.rotateRightAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - (w - r)))
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.smallSchroder.eq_1 : Nat.smallSchroder 0 = 1
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.isClosed_ball : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x : X) (r : ℝ), IsClosed (Metric.ball x r)
-- Mathlib.Algebra.Ring.IsFormallyReal
isSumNonzeroSq_iff_isSumSq : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] {s : R}, s ≠ 0 → (IsSumNonzeroSq s ↔ IsSumSq s)
-- Mathlib.Algebra.Order.Pi
Pi.single_pos : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (α i)]
  [inst_2 : (i : ι) → Preorder (α i)] {i : ι} {a : α i}, 0 < Pi.single i a ↔ 0 < a
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_pt : ∀ {α : Type u} {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J]
  [inst_2 : SemilatticeInf α] [inst_3 : OrderTop α] (F : CategoryTheory.Functor J α),
  (CategoryTheory.Limits.CompleteLattice.finiteLimitCone F).cone.pt = Finset.univ.inf F.obj
-- Mathlib.Analysis.Calculus.Deriv.Inv
derivWithin_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜},
  x ≠ 0 → UniqueDiffWithinAt 𝕜 s x → derivWithin (fun x => x⁻¹) s x = -(x ^ 2)⁻¹
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.State.mk : Lean.PrettyPrinter.Delaborator.OptionsPerPos →
  Array (Lean.Expr × Lean.Expr) → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.State
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.const_smul : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : SMul M X] {m : MeasurableSpace α}
  {g : α → X} [MeasurableConstSMul M X], Measurable g → ∀ (c : M), Measurable (c • g)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pushoutIsoOpPullback_inl_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.Limits.pushoutIsoOpPullback f g).hom =
    (CategoryTheory.Limits.pullback.fst f.unop g.unop).op
-- Mathlib.Data.Sym.Sym2
Sym2.other_ne : ∀ {α : Type u_1} {a : α} {z : Sym2 α}, ¬z.IsDiag → ∀ (h : a ∈ z), Sym2.Mem.other h ≠ a