mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.decl.inj : ∀ {xs : Array Lean.Elab.Term.Do.Var} {doElem : Lean.Syntax} {k : Lean.Elab.Term.Do.Code}
  {xs_1 : Array Lean.Elab.Term.Do.Var} {doElem_1 : Lean.Syntax} {k_1 : Lean.Elab.Term.Do.Code},
  Lean.Elab.Term.Do.Code.decl xs doElem k = Lean.Elab.Term.Do.Code.decl xs_1 doElem_1 k_1 →
    xs = xs_1 ∧ doElem = doElem_1 ∧ k = k_1
-- Mathlib.AlgebraicGeometry.Spec
/-- The spectrum of a commutative ring, as a `LocallyRingedSpace`.  -/
AlgebraicGeometry.Spec.locallyRingedSpaceObj : CommRingCat → AlgebraicGeometry.LocallyRingedSpace
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationFiniteSpanTarget`
if `P` holds for `R →+* S` whenever there exists a finite set `{ r }` that spans `S` such that
`P` holds for `R →+* Sᵣ`.

Note that this is equivalent to `RingHom.OfLocalizationSpanTarget` via
`RingHom.ofLocalizationSpanTarget_iff_finite`, but this is easier to prove.  -/
RingHom.OfLocalizationFiniteSpanTarget : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.nil.eq_1 : Turing.ToPartrec.Code.nil = Turing.ToPartrec.Code.tail.comp Turing.ToPartrec.Code.succ
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegrable_sub_inv_iff : ∀ {c w : ℂ} {R : ℝ}, CircleIntegrable (fun z => (z - w)⁻¹) c R ↔ R = 0 ∨ w ∉ Metric.sphere c |R|
-- Mathlib.Data.Matrix.Mul
Matrix.vecMulVec_add : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Mul α] [inst_1 : Add α] [LeftDistribClass α] (w : m → α)
  (v₁ v₂ : n → α), Matrix.vecMulVec w (v₁ + v₂) = Matrix.vecMulVec w v₁ + Matrix.vecMulVec w v₂
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.ext_ring_iff : ∀ {R : Type u_10} [inst : Semiring R] {S : Type u_11} [inst_1 : Semiring S] {N' : Type u_13} [inst_2 : AddMonoid N']
  [inst_3 : DistribMulAction S N'] {σ : R →* S} {f g : R →ₑ+[σ] N'}, f = g ↔ f 1 = g 1
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mkAux.eq_2 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0)
  (n : ℕ),
  ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n.succ =
    { X₁ := (succ (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).fst,
      X₂ := (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₁, X₃ := (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₂,
      f := (succ (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst,
      g := (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n).f, zero := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_right_unitor_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) {Z : ↑(self.obj b)} (h : (self.map f).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.id b)).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.mapId b).hom.toNatTrans.app ((self.map f).toFunctor.obj X)) h)
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiffTag.toString : Lean.Widget.ExprDiffTag✝ → String
-- Init.Data.Vector.Count
Vector.count_replicate_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {n : ℕ}, Vector.count a (Vector.replicate n a) = n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe_toReal : ∀ (θ : Real.Angle), ↑θ.toReal = θ
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.forall_mem_adjoin_smul_eq_self_iff : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Set A)
  {M : Type u_1} [inst_3 : Monoid M] [inst_4 : MulSemiringAction M A] [SMulCommClass M R A] (m : M),
  (∀ x ∈ Algebra.adjoin R S, m • x = x) ↔ ∀ x ∈ S, m • x = x
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
MeasureTheory.condExp_ae_eq_restrict_zero : ∀ {α : Type u_1} {E : Type u_2} {m m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} {s : Set α},
  MeasurableSet s → f =ᵐ[μ.restrict s] 0 → μ[f | m] =ᵐ[μ.restrict s] 0
-- Mathlib.Algebra.MvPolynomial.Comap
MvPolynomial.comap_id_apply : ∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R] (x : σ → R),
  MvPolynomial.comap (AlgHom.id R (MvPolynomial σ R)) x = x
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafFunctor_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A] {X Y : A}
  (f : X ⟶ Y) (j : Cᵒᵖ), (Φ.skyscraperPresheafFunctor.map f).app j = CategoryTheory.Limits.Pi.map fun x => f
-- Lean.Meta.Sym.Eta
Lean.Meta.Sym.etaReduceWithCache : Lean.Expr →
  Std.HashMap Lean.Meta.Sym.ExprPtr Lean.Expr → Lean.CoreM (Lean.Expr × Std.HashMap Lean.Meta.Sym.ExprPtr Lean.Expr)
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.map.match_1.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3) (a a_1 : C)
  (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1)
  (h_1 :
    (a a_2 : C) →
      (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_2) →
        motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_2) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_2, f => h_1 a a_2 f
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => h_2 a x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_1 a a_1 f
-- Mathlib.Analysis.Convex.Integral
/-- **Jensen's inequality**, strict version: if an integrable function `f : α → E` takes values in a
convex closed set `s`, and `g : E → ℝ` is continuous and strictly concave on `s`, then
either `f` is a.e. equal to its average value, or `⨍ x, g (f x) ∂μ < g (⨍ x, f x ∂μ)`.  -/
StrictConcaveOn.ae_eq_const_or_lt_map_average : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  StrictConcaveOn ℝ s g →
    ContinuousOn g s →
      IsClosed s →
        (∀ᵐ (x : α) ∂μ, f x ∈ s) →
          MeasureTheory.Integrable f μ →
            MeasureTheory.Integrable (g ∘ f) μ →
              f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), g (f x) ∂μ < g (⨍ (x : α), f x ∂μ)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesOnBall.hasSum_iteratedFDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r →
    ∀ [CompleteSpace F] [CharZero 𝕜] {y : E},
      y ∈ Metric.eball 0 r → HasSum (fun n => (↑n.factorial)⁻¹ • (iteratedFDeriv 𝕜 n f x) fun x => y) (f (x + y))
-- Std.Time.DateTime
/-- Add `Year.Offset` to a `DateTime`, rolling over excess days.
 -/
Std.Time.DateTime.addYearsRollOver : Std.Time.DateTime → Std.Time.Year.Offset → Std.Time.DateTime
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.toFractionRingRingEquiv_apply : ∀ (K : Type u) [inst : CommRing K] (self : RatFunc K), (RatFunc.toFractionRingRingEquiv K) self = self.toFractionRing
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.sk.faithful : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (n : ℕ)
  [inst_1 :
    ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F]
  [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F],
  (CategoryTheory.SimplicialObject.Truncated.sk n).Faithful
-- Mathlib.Algebra.Star.SelfAdjoint
IsStarNormal.map : ∀ {F : Type u_3} {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Star R] [inst_2 : Mul S] [inst_3 : Star S]
  [inst_4 : FunLike F R S] [MulHomClass F R S] [StarHomClass F R S] (f : F) (r : R) [hr : IsStarNormal r],
  IsStarNormal (f r)
-- Mathlib.Algebra.Homology.CochainComplexPlus
CategoryTheory.Functor.mapCochainComplexPlus_obj_obj_d : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  [inst_4 : F.PreservesZeroMorphisms] (X : CochainComplex.Plus C) (i j : ℤ),
  (F.mapCochainComplexPlus.obj X).obj.d i j = F.map (X.obj.d i j)
-- Std.Net.Addr
Std.Net.IPv4Addr.mk : Vector UInt8 4 → Std.Net.IPv4Addr
-- Lean.Parser.Command
Lean.Parser.Command.optDefDeriving.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_strict_mono_left : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : PartialOrder k] [IsOrderedRing k] [inst_3 : AddCommGroup E]
  [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E] [IsStrictOrderedModule k E] {a a' b : E}
  {r : k}, a < a' → r < 1 → (AffineMap.lineMap a b) r < (AffineMap.lineMap a' b) r
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_insertListConst_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' fallback : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert →
          k ∈ List.map Prod.fst toInsert →
            Std.Internal.List.getKeyD k' (Std.Internal.List.insertListConst l toInsert) fallback = k
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- Make a morphism in `SimplexCategory` from a monotone map of `Fin`'s.  -/
SimplexCategory.Hom.mk : {a b : SimplexCategory} → (Fin (a.len + 1) →o Fin (b.len + 1)) → a.Hom b
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.directiveExpandersForUnsafe : Lean.Ident →
  Lean.Elab.TermElabM
    (Array
      (Lean.Name ×
        (Lean.TSyntaxArray `block →
          StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to `X₁`.  -/
CategoryTheory.Limits.ChosenPullback₃.p₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          {f₃ : X₃ ⟶ S} →
            {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} →
              {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃} →
                {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} →
                  (self : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) → self.chosenPullback.pullback ⟶ X₁
-- Init.Data.Float.Model.Unpacked.Round
Float.Model.UnpackedFloat.ExtendedMantissa.mk.inj : ∀ {mantissa : ℕ} {roundBit stickyBit : Bool} {mantissa_1 : ℕ} {roundBit_1 stickyBit_1 : Bool},
  { mantissa := mantissa, roundBit := roundBit, stickyBit := stickyBit } =
      { mantissa := mantissa_1, roundBit := roundBit_1, stickyBit := stickyBit_1 } →
    mantissa = mantissa_1 ∧ roundBit = roundBit_1 ∧ stickyBit = stickyBit_1
-- Init.SimpLemmas
true_and : ∀ (p : Prop), (True ∧ p) = p
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isColoop_iff_sdiff_closure : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsColoop e ↔ M.closure (M.E \ {e}) ≠ M.E
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Real.Angle.toCircle_zero : Real.Angle.toCircle 0 = 1
-- Lean.Meta.Constructions.CtorIdx
Lean.mkToCtorIdxName : Lean.Name → Lean.Name
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidRevSearchFrom.startPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice},
  String.Slice.Pattern.Model.IsValidRevSearchFrom pat s.startPos []
-- Mathlib.Tactic.GCongr.ForwardAttr
Mathlib.Tactic.GCongr.ForwardExt.mk.injEq : ∀ (eval eval_1 : Lean.Expr → Lean.MVarId → Lean.MetaM Unit), ({ eval := eval } = { eval := eval_1 }) = (eval = eval_1)
-- Mathlib.Algebra.Group.Nat.Even
Nat.two_mul_div_two_of_even : ∀ {n : ℕ}, Even n → 2 * (n / 2) = n
-- Mathlib.Topology.UniformSpace.Basic
Uniform.continuousWithinAt_iff'_left : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : TopologicalSpace β] {f : β → α} {b : β} {s : Set β},
  ContinuousWithinAt f s b ↔ Filter.Tendsto (fun x => (f x, f b)) (nhdsWithin b s) (uniformity α)
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
LinearEquiv.coe_isometryOfOrthonormal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E')
  {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)), ⇑(f.isometryOfOrthonormal hv hf) = ⇑f
-- Lean.Util.NumObjs
/-- Returns the number of allocated `Expr` objects in the given expression `e`.

This operation is performed in `IO` because the result depends on the memory representation of the object.

Note: Use this function primarily for diagnosing performance issues.
 -/
Lean.Expr.numObjs : Lean.Expr → IO ℕ
-- Init.Data.BitVec.Lemmas
BitVec.sshiftRight_add : ∀ {w : ℕ} {x : BitVec w} {m n : ℕ}, x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.instFaithfulTopCatCompHausLikeToTop : ∀ (P : TopCat → Prop), (CompHausLike.compHausLikeToTop P).Faithful
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolRing_one : ∀ {α : Type u_1} [inst : BooleanAlgebra α], ofBoolRing 1 = ⊤
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.«builder_option(Immediate:=[_])» : Lean.ParserDescr
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.mk.sizeOf_spec : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : SizeOf ι]
  [inst_3 : (a : ι) → SizeOf (G a)] [inst_4 : SizeOf H] (toWord : Monoid.CoprodI.Word G) (head : H)
  (normalized : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ toWord.toList → g ∈ d.set i),
  sizeOf { toWord := toWord, head := head, normalized := normalized } = 1 + sizeOf toWord + sizeOf head
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (F : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) {X Y : SimplexCategory} (f : X ⟶ Y),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.functor.obj F).right.map f =
    F.map (CategoryTheory.WithInitial.incl.map f)
-- Std.Time.Zoned.ZoneRules
/-- Gets the `TimeZone` offset from a `LocalTimeType`.
 -/
Std.Time.TimeZone.LocalTimeType.getTimeZone : Std.Time.TimeZone.LocalTimeType → Std.Time.TimeZone
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.abs_lt_one_iff : ∀ {a : ℤ}, |a| < 1 ↔ a = 0
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
ciInf_eq_univ_of_not_bddBelow : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {f : ι → α},
  ¬BddBelow (Set.range f) → ⨅ i, f i = sInf Set.univ
-- Mathlib.Data.List.Map2
List.zipWith_flip : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (as : List α) (bs : List β),
  List.zipWith (flip f) bs as = List.zipWith f as bs
-- Mathlib.Tactic.Basic
/-- Messages produced by the executed tactic.  -/
Mathlib.Tactic.withResetServerInfo.Result.msgs : {α : Type} → Mathlib.Tactic.withResetServerInfo.Result α → Lean.MessageLog
-- Mathlib.CategoryTheory.Sites.InducedTopology
CategoryTheory.Precoverage.toGrothendieck_comap_le_restrictedTopology : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (K : CategoryTheory.Precoverage D),
  (CategoryTheory.Precoverage.comap F K).toGrothendieck ≤ F.restrictedTopology K.toGrothendieck
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_empty : ∀ {α : Type u_1} {s : Set α}, s \ ∅ = s
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.self_comp_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  ⇑h ∘ ⇑h.symm = id
-- Mathlib.MeasureTheory.Integral.Bochner.L1
_private.Mathlib.MeasureTheory.Integral.Bochner.L1.0.MeasureTheory.«term_→ₛ_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Adjoin.Field
/-- Produce an algebra homomorphism `Adjoin R {x} →ₐ[R] T` sending `x` to
a root of `x`'s minimal polynomial in `T`.  -/
Algebra.adjoin.liftSingleton : (F : Type u_1) →
  [inst : Field F] →
    {S : Type u_2} →
      {T : Type u_3} →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra F S] →
              [inst_4 : Algebra F T] → (x : S) → (y : T) → (Polynomial.aeval y) (minpoly F x) = 0 → ↥F[x] →ₐ[F] T
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE._auto_3),
  (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f₃)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.entryAtIdxD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {i : ℕ}
  {fallback : α × β}, t₁.Equiv t₂ → t₁.entryAtIdxD i fallback = t₂.entryAtIdxD i fallback
-- Mathlib.RingTheory.LinearDisjoint
/-- Linear disjointness is symmetric if elements in the module commute.  -/
Subalgebra.linearDisjoint_comm_of_commute : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  (∀ (a : ↥A) (b : ↥B), Commute ↑a ↑b) → (A.LinearDisjoint B ↔ B.LinearDisjoint A)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.length : Lean.Grind.CommRing.Mon → ℕ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_eq_fallback : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α} {fallback : β}, a ∉ t → Std.ExtDTreeMap.Const.getD t a fallback = fallback
-- Mathlib.SetTheory.Cardinal.Subfield
_private.Mathlib.SetTheory.Cardinal.Subfield.0.Subfield.rangeOfWType_eq_top : ∀ {α : Type u} (s : Set α) [inst : DivisionRing α], Subfield.rangeOfWType✝ s = ⊤
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.instIsIsoHomOfMapForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.AddMon C} (f : A ⟶ B) [e : CategoryTheory.IsIso ((CategoryTheory.AddMon.forget C).map f)],
  CategoryTheory.IsIso f.hom
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- If a functor preserves a certain left homology data of a short complex `S`, then it
preserves the left homology of `S`.  -/
CategoryTheory.Functor.PreservesLeftHomologyOf.mk' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [h.IsPreservedBy F],
  F.PreservesLeftHomologyOf S
-- Mathlib.Algebra.Homology.Homotopy
CategoryTheory.Functor.mapHomotopyEquiv_homotopyInvHomId : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} W]
  [inst_3 : CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [inst_4 : F.Additive]
  (h : HomotopyEquiv C D), (F.mapHomotopyEquiv h).homotopyInvHomId = ⋯.mpr (⋯.mpr (F.mapHomotopy h.homotopyInvHomId))
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
/-- If `F : C ⥤ D` is dense at `Y : D` and `G : D ⥤ D'` is an equivalence,
then `F ⋙ G` is dense at `G.obj Y`.  -/
CategoryTheory.Functor.DenseAt.postcompEquivalence : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {Y : D} →
            F.DenseAt Y →
              {D' : Type u_1} →
                [inst_2 : CategoryTheory.Category.{v_1, u_1} D'] →
                  (G : CategoryTheory.Functor D D') → [G.IsEquivalence] → (F.comp G).DenseAt (G.obj Y)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.openRcNhdsToCompactNhds_mono : ∀ {α : Type u_1} [inst : TopologicalSpace α] (K : TopologicalSpace.Compacts α), Monotone K.openRcNhdsToCompactNhds
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.NatTrans.sum'_app_inr : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor A C}
  {H I : CategoryTheory.Functor B C} (α : F ⟶ G) (β : H ⟶ I) (b : B),
  (CategoryTheory.NatTrans.sum' α β).app (Sum.inr b) = β.app b
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
DirectedOn.le_csSup_of_le : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {s : Set α} {a b : α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → BddAbove s → b ∈ s → a ≤ b → a ≤ sSup s
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instHashableRange.hash : Lean.Lsp.Range → UInt64