mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_map_right_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (Y : T) (X : D)
  {X_1 Y_1 : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)} (g : X_1 ⟶ Y_1),
  ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).map g).right.right =
    CategoryTheory.Under.Hom.right g.right
-- Mathlib.NumberTheory.ClassNumber.Finite
ClassGroup.finsetApprox.zero_notMem : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (bS : Module.Basis ι R S) (adm : abv.IsAdmissible) [inst_6 : Infinite R] [inst_7 : DecidableEq R],
  0 ∉ ClassGroup.finsetApprox bS adm
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.Cont.eval.match_1.eq_1 : ∀ (motive : Turing.ToPartrec.Cont → Sort u_1) (h_1 : Unit → motive Turing.ToPartrec.Cont.halt)
  (h_2 :
    (fs : Turing.ToPartrec.Code) →
      (as : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₁ fs as k))
  (h_3 : (ns : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₂ ns k))
  (h_4 : (f : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.comp f k))
  (h_5 : (f : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.fix f k)),
  (match Turing.ToPartrec.Cont.halt with
    | Turing.ToPartrec.Cont.halt => h_1 ()
    | Turing.ToPartrec.Cont.cons₁ fs as k => h_2 fs as k
    | Turing.ToPartrec.Cont.cons₂ ns k => h_3 ns k
    | Turing.ToPartrec.Cont.comp f k => h_4 f k
    | Turing.ToPartrec.Cont.fix f k => h_5 f k) =
    h_1 ()
-- Mathlib.Data.Set.Monotone
StrictAntiOn.congr : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  StrictAntiOn f₁ s → Set.EqOn f₁ f₂ s → StrictAntiOn f₂ s
-- Mathlib.Order.RelIso.Basic
RelHom.swap_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) (a : α), f.swap a = f a
-- Init.System.ST
ST.Ref.mk : {σ α : Type} → ST.RefPointed.type → Nonempty α → ST.Ref σ α
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.toCostructuredArrow_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y),
  (CategoryTheory.Limits.Cone.toCostructuredArrow F).map f = CategoryTheory.CostructuredArrow.homMk f.hom ⋯
-- Mathlib.Data.FunLike.Group
FunLike.coeMonoidHom.eq_1 : ∀ (F : Type u_1) (α : Type u_2) (β : Type u_3) [inst : FunLike F α β] [inst_1 : MulOne F] [inst_2 : MulOneClass β]
  [inst_3 : IsOneApply F α β] [inst_4 : IsMulApply F α β],
  FunLike.coeMonoidHom F α β = { toFun := fun f => ⇑f, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.hom_id : ∀ {X : GrpWithZero},
  CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X) = MonoidWithZeroHom.id X.carrier
-- Aesop.Rule.Basic
Aesop.Rule.mk : {α : Type} → Aesop.RuleName → Aesop.IndexingMode → Option Aesop.RulePattern → α → Aesop.RuleTacDescr → Aesop.Rule α
-- Mathlib.Combinatorics.Graph.Basic
Graph.Inc.vertex_mem : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, G.Inc e x → x ∈ G.vertexSet
-- Init.Prelude
/-- Either a proof that `p` is true or a proof that `p` is false. This is equivalent to a `Bool` paired
with a proof that the `Bool` is `true` if and only if `p` is true.

`Decidable` instances are primarily used via `if`-expressions and the tactic `decide`. In
conditional expressions, the `Decidable` instance for the proposition is used to select a branch. At
run time, this case distinction code is identical to that which would be generated for a
`Bool`-based conditional. In proofs, the tactic `decide` synthesizes an instance of `Decidable p`,
attempts to reduce it to `isTrue h`, and then succeeds with the proof `h` if it can.

Because `Decidable` carries data, when writing `@[simp]` lemmas which include a `Decidable` instance
on the LHS, it is best to use `{_ : Decidable p}` rather than `[Decidable p]` so that non-canonical
instances can be found via unification rather than instance synthesis.
 -/
Decidable : Prop → Type
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.coeFn_neg : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] (f : ↥(lp E p)),
  ↑(-f) = -↑f
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.AuxLemmaKey.defeq : Lean.Meta.AuxLemmaKey → Bool
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNormal.eq_def : ∀ (x : Turing.ToPartrec.Code) (x_1 : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.trNormal x x_1 =
    match x, x_1 with
    | Turing.ToPartrec.Code.zero', k =>
      Turing.PartrecToTM2.Λ'.push Turing.PartrecToTM2.K'.main (fun x => some Turing.PartrecToTM2.Γ'.cons)
        (Turing.PartrecToTM2.Λ'.ret k)
    | Turing.ToPartrec.Code.succ, k =>
      Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.Λ'.ret k).succ
    | Turing.ToPartrec.Code.tail, k =>
      Turing.PartrecToTM2.Λ'.clear Turing.PartrecToTM2.natEnd Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.Λ'.ret k)
    | f.cons fs, k =>
      Turing.PartrecToTM2.Λ'.push Turing.PartrecToTM2.K'.stack (fun x => some Turing.PartrecToTM2.Γ'.consₗ)
        (Turing.PartrecToTM2.Λ'.move (fun x => false) Turing.PartrecToTM2.K'.main Turing.PartrecToTM2.K'.rev
          (Turing.PartrecToTM2.trNormal f (Turing.PartrecToTM2.Cont'.cons₁ fs k)).copy)
    | f.comp g, k => Turing.PartrecToTM2.trNormal g (Turing.PartrecToTM2.Cont'.comp f k)
    | f.case g, k => (Turing.PartrecToTM2.trNormal f k).pred (Turing.PartrecToTM2.trNormal g k)
    | f.fix, k => Turing.PartrecToTM2.trNormal f (Turing.PartrecToTM2.Cont'.fix f k)
-- Mathlib.Analysis.SumIntegralComparisons
sum_Ico_le_integral_of_le : ∀ {a b : ℕ} {f g : ℝ → ℝ},
  a ≤ b →
    (∀ i ∈ Set.Ico a b, ∀ x ∈ Set.Ico ↑i ↑(i + 1), f ↑i ≤ g x) →
      MeasureTheory.IntegrableOn g (Set.Ico ↑a ↑b) MeasureTheory.volume →
        ∑ i ∈ Finset.Ico a b, f ↑i ≤ ∫ (x : ℝ) in ↑a..↑b, g x
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.cardinal_eq : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E],
  Cardinal.mk (Field.Emb F E) = (fun c => if Cardinal.aleph0 ≤ c then 2 ^ c else c) (Field.sepDegree F E)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.inv.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f f_1 : CauSeq β abv) (e_f : f = f_1)
  (hf : ¬f.LimZero), f.inv hf = f_1.inv ⋯
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The distance from the orthocenter to the reflection of the
circumcenter in a side equals the circumradius, variant using a
`Finset`.  -/
Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ : Fin 3},
  i₁ ≠ i₂ →
    dist t.orthocenter
        ((EuclideanGeometry.reflection (affineSpan ℝ (t.points '' ↑{i₁, i₂}))) (Affine.Simplex.circumcenter t)) =
      Affine.Simplex.circumradius t
-- Mathlib.CategoryTheory.Category.Cat
/-- The type of 2-morphisms in the bicategory of categories `Cat`.
This is a wrapper around `NatTrans` to prevent defeq-abuse.
 -/
CategoryTheory.Cat.Hom₂ : {C D : CategoryTheory.Cat} → (C ⟶ D) → (C ⟶ D) → Type (max u v)
-- Mathlib.RingTheory.Norm.Defs
Algebra.norm_eq_one_of_not_exists_basis : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S],
  (¬∃ s, Nonempty (Module.Basis (↥s) R S)) → ∀ (x : S), (Algebra.norm R) x = 1
-- Mathlib.Geometry.Manifold.Algebra.Monoid
mdifferentiable_add_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I 1 G] {a : G},
  MDiff fun x => a + x
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.embedding.eq_1 : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : GroupWithZero B] {f : A →*₀ B},
  MonoidWithZeroHom.ValueGroup₀.embedding =
    (MonoidWithZeroHom.ofClass WithZero.withZeroUnitsEquiv).comp (WithZero.map' f.valueGroup.subtype)
-- Mathlib.Analysis.Fourier.FourierTransform
Real.Lp.fourierTransformInv_toLp : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  {f : V → E} (hf : MeasureTheory.MemLp f 1 MeasureTheory.volume),
  ⇑(Real.Lp.fourierTransformInv (MeasureTheory.MemLp.toLp f hf)) = FourierTransformInv.fourierInv f
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_congr : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a b : α}, (a == b) = true → m.contains a = m.contains b
-- Mathlib.CategoryTheory.Limits.Sifted
/-- A nonempty category with binary coproducts is sifted.  -/
CategoryTheory.IsSifted.isSifted_of_hasBinaryCoproducts_and_nonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [Nonempty C] [CategoryTheory.Limits.HasBinaryCoproducts C],
  CategoryTheory.IsSifted C
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.FilterMap.mk.sizeOf_spec : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α}
  {f : β → Std.Iterators.PostconditionT n (Option γ)} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf γ]
  [inst_3 : (a : Type w) → SizeOf (m a)] [inst_4 : (a : Type w) → SizeOf (n a)] (inner : Std.IterM m β),
  sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.equivQuotientSubgroupOfOfEq.eq_1 : ∀ {G : Type u} [inst : Group G] {A' A B' B : Subgroup G} [hAN : (A'.subgroupOf A).Normal]
  [hBN : (B'.subgroupOf B).Normal] (h' : A' = B') (h : A = B),
  QuotientGroup.equivQuotientSubgroupOfOfEq h' h =
    (QuotientGroup.quotientMapSubgroupOfOfLe ⋯ ⋯).toMulEquiv (QuotientGroup.quotientMapSubgroupOfOfLe ⋯ ⋯) ⋯ ⋯
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_monomial : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (i : ℕ) (k : R),
  (Polynomial.taylor r) ((Polynomial.monomial i) k) = Polynomial.C k * (Polynomial.X + Polynomial.C r) ^ i
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.instHasSmallObjectArgumentJ : SSet.modelCategoryQuillen.J.HasSmallObjectArgument
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
norm_fderiv_iteratedFDeriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {n : ℕ}, ‖fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖
-- Init.Data.Iterators.Basic
Std.IterM.TerminationMeasures.Productive.mk.inj : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {inst : Std.Iterator α m β} {it it_1 : Std.IterM m β},
  { it := it } = { it := it_1 } → it = it_1
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_sum_of_nonneg : ∀ {ι : Type u_1} {a : ℝ}, 0 ≤ a → ∀ {s : Finset ι} {f : ι → ℝ}, (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ico_castAdd : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n),
  ∑ i ∈ Finset.Ico (Fin.castAdd m a) (Fin.castAdd m b), f i = ∑ i ∈ Finset.Ico a b, f (Fin.castAdd m i)
-- Lean.Elab.Tactic.Ext
_private.Lean.Elab.Tactic.Ext.0.Lean.Elab.Tactic.Ext.evalExt : Lean.Elab.Tactic.Tactic
-- Mathlib.Data.Nat.ChineseRemainder
Nat.chineseRemainderOfList.eq_1 : ∀ {ι : Type u_1} (a s : ι → ℕ) (x_2 : List.Pairwise (Function.onFun Nat.Coprime s) []),
  Nat.chineseRemainderOfList a s [] x_2 = ⟨0, ⋯⟩
-- Mathlib.ModelTheory.Syntax
/-- The implication between two bounded formulas.  -/
FirstOrder.Language.BoundedFormula.imp : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `insertIfNew` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.insertIfNewₘ : {α : Type u} →
  {β : α → Type v} →
    [Ord α] → (k : α) → β k → (l : Std.DTreeMap.Internal.Impl α β) → l.Balanced → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.GrpCat.Hom.mk.sizeOf_spec : ∀ {A B : GrpCat} (hom' : ↑A →* ↑B), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mk : {ι : Type u_1} →
  {I : BoxIntegral.Box ι} →
    (boxes : Finset (BoxIntegral.Box ι)) →
      (∀ J ∈ boxes, J ≤ I) →
        (↑boxes).Pairwise (Function.onFun Disjoint BoxIntegral.Box.toSet) → BoxIntegral.Prepartition I
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset : ∀ {X : AlgebraicGeometry.Scheme} {x : ↥X} {U : X.Opens},
  x ∈ U → ∃ R f, AlgebraicGeometry.IsOpenImmersion f ∧ x ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑U
-- Mathlib.MeasureTheory.Integral.Average
/-- Average value of an `ℝ≥0∞`-valued function `f` w.r.t. a measure `μ`.

It is equal to `(μ univ)⁻¹ * ∫⁻ x, f x ∂μ`, so it takes value zero if `μ` is an infinite measure. If
`μ` is a probability measure, then the average of any function is equal to its integral.

For the average on a set, use `⨍⁻ x in s, f x ∂μ`, defined as `⨍⁻ x, f x ∂(μ.restrict s)`. For the
average w.r.t. the volume, one can omit `∂volume`.  -/
MeasureTheory.«term⨍⁻_,_∂_» : Lean.ParserDescr
-- Init.Prelude
instNonemptyOfInhabited : ∀ {α : Sort u} [Inhabited α], Nonempty α
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isBounded_of_abs_le : ∀ {α : Type u_3} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [inst_3 : PseudoMetricSpace α]
  [CompactIccSpace α] (C : α), Bornology.IsBounded {x | |x| ≤ C}
-- Mathlib.LinearAlgebra.Alternating.DomCoprod
AlternatingMap.domCoprod'_apply : ∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
  {N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
  [inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂),
  AlternatingMap.domCoprod' (a ⊗ₜ[R'] b) = a.domCoprod b
-- Mathlib.Topology.Algebra.Order.Archimedean
/-- Rational numbers are dense in a linear ordered archimedean field.  -/
Rat.denseRange_cast : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] [Archimedean 𝕜], DenseRange Rat.cast
-- Mathlib.Algebra.Order.Module.Defs
nonneg_of_smul_nonneg_of_pos_right : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosReflectLE α β], 0 ≤ a • b → 0 < b → 0 ≤ a
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.range_exp_mul_I : (Set.range fun x => Complex.exp (↑x * Complex.I)) = Metric.sphere 0 1
-- Init.Data.Float.Model.Unpacked.Sign
/-- Converts the sign to a bitvector, with positive sign denoted by `0`.
 -/
Float.Model.UnpackedFloat.Sign.toBitVec : Float.Model.UnpackedFloat.Sign → BitVec 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k k' : α},
  m.WF → m.getKey? k = some k' → (Std.HashMap.Raw.map f m)[k]? = Option.map (f k') m[k]?
-- Mathlib.Data.Rat.Cast.CharZero
Rat.cast_mul : ∀ {α : Type u_3} [inst : DivisionRing α] [CharZero α] (p q : ℚ), ↑(p * q) = ↑p * ↑q
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.instCoeDep : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        (X : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) →
          CoeDep (CategoryTheory.PreGaloisCategory.PointedGaloisObject F) X C
-- Mathlib.Data.Finset.Disjoint
Finset.pairwiseDisjoint_coe : ∀ {α : Type u_2} {ι : Type u_5} {s : Set ι} {f : ι → Finset α},
  (s.PairwiseDisjoint fun i => ↑(f i)) ↔ s.PairwiseDisjoint f
-- Std.Internal.UV.System
Std.Internal.UV.System.PasswdInfo.shell : Std.Internal.UV.System.PasswdInfo → Option String
-- Init.Data.Iterators.Combinators.Monadic.Take
/-- This combinator is only useful for advanced use cases.

Given a finite iterator `it`, returns an iterator that behaves exactly like `it` but is of the same
type as `it.take n`.

**Marble diagram:**

```text
it          ---a----b---c--d-e--⊥
it.toTake   ---a----b---c--d-e--⊥
```

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it`.
 -/
Std.IterM.toTake : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → [inst : Std.Iterator α m β] → [Std.Iterators.Finite α m] → Std.IterM m β → Std.IterM m β
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- Binet's formula as a function equality.  -/
Real.coe_fib_eq' : (fun n => ↑(Nat.fib n)) = fun n => (Real.goldenRatio ^ n - Real.goldenConj ^ n) / √5
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cyclesIso₀_comp_H0π_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑(groupHomology.cycles A 0)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H0π A))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.cyclesIso₀ A).hom) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.π A 0)) x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {l : List (α × β)},
  (t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.smul_continuous : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] {𝕜 : Type u_9}
  [inst_6 : NormedRing 𝕜] [inst_7 : Module 𝕜 E] [NormSMulClass 𝕜 E] [SecondCountableTopologyEither X E] {f : X → 𝕜}
  {g : X → E},
  Continuous g → MeasureTheory.LocallyIntegrable f μ → MeasureTheory.LocallyIntegrable (fun x => f x • g x) μ
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.norm_integral_le_lintegral_norm : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  ‖∫ᵛ (a : X), f a ∂[B; μ]‖ ≤ ‖B‖ * (∫⁻ (a : X), ENNReal.ofReal ‖f a‖ ∂μ.variation).toReal
-- Init.Data.Order.Ord
List.instTransCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp], Std.TransCmp (List.compareLex cmp)
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivWithinAt.add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → HasDerivWithinAt g g' s x → HasDerivWithinAt (f + g) (f' + g') s x
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.IsFraisse.is_essentially_countable : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [self : FirstOrder.Language.IsFraisse K],
  (Quotient.mk' '' K).Countable
-- Init.Data.Nat.Basic
Nat.lt_add_right : ∀ {a b : ℕ} (c : ℕ), a < b → a < b + c
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.instNonemptyElemFreeAddMonoidProdForallLifts : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (x : PiTensorProduct R fun i => s i), Nonempty ↑x.lifts
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
DirectSum.toAddMonoidAlgebra_zero : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring M] [inst_2 : (m : M) → Decidable (m ≠ 0)],
  DirectSum.toAddMonoidAlgebra 0 = 0
-- Mathlib.Condensed.Equivalence
/-- The equivalence from coherent sheaves on `Stonean` to coherent sheaves on `CompHaus`
(i.e. condensed sets).  -/
Condensed.StoneanCompHaus.equivalence : (A : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [∀ (X : CompHausᵒᵖ),
          CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A] →
      CategoryTheory.Sheaf (CategoryTheory.coherentTopology Stonean) A ≌ Condensed A
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_eraseₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {a : α},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.Raw.WFImp ↑(m.eraseₘ a)
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_neg_atTop_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] {l : Filter α}
  {f : α → G}, Filter.Tendsto (fun x => -f x) l Filter.atTop ↔ Filter.Tendsto f l Filter.atBot
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.HasLift.iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g), sq.HasLift ↔ Nonempty sq.LiftStruct
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.addCommMonoid : {α : Type u_1} → [inst : AddCommMonoid α] → [inst_1 : Preorder α] → [AddLeftMono α] → AddCommMonoid { x // 0 ≤ x }
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- A version of σ_comp_σ with indices in ℕ satisfying relevant inequalities.  -/
SimplexCategoryGenRel.σ_comp_σ_nat : ∀ {n : ℕ} (i j : ℕ) (hi : i < n + 1) (hj : j < n + 1),
  i ≤ j →
    CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ ⟨i, ⋯⟩) (SimplexCategoryGenRel.σ ⟨j, hj⟩) =
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ ⟨j + 1, ⋯⟩) (SimplexCategoryGenRel.σ ⟨i, hi⟩)
-- Init.Data.Range.Polymorphic.PRange
/-- Every element of the intersection is an element of both original ranges.
   -/
Std.Roc.LawfulRcoIntersection.mem_intersection_iff : ∀ {α : Type w} {inst : LT α} {inst_1 : LE α} {inst_2 : Std.Roc.HasRcoIntersection α}
  [self : Std.Roc.LawfulRcoIntersection α] {a : α} {r : Std.Roc α} {s : Std.Rco α},
  a ∈ Std.Roc.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coeRingHom_toFun : ∀ (x : ℝ), Hyperreal.coeRingHom x = ↑x
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformlyOn.sub : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β},
  TendstoUniformlyOn f g l s → TendstoUniformlyOn f' g' l s → TendstoUniformlyOn (f - f') (g - g') l s