mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- The pushout-product is associative: `(X₁ □ X₂) □ X₃ ≅ X₁ □ X₂ □ X₃`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPushouts C] →
      [inst_2 : CategoryTheory.MonoidalCategory C] →
        (X₁ X₂ X₃ : CategoryTheory.Arrow C) →
          [CategoryTheory.Limits.PreservesColimit
                (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
                (CategoryTheory.MonoidalCategory.tensorRight X₃.left)] →
            [CategoryTheory.Limits.PreservesColimit
                  (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
                  (CategoryTheory.MonoidalCategory.tensorRight X₃.right)] →
              [CategoryTheory.Limits.PreservesColimit
                    (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
                      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom))
                    (CategoryTheory.MonoidalCategory.tensorLeft X₁.left)] →
                [CategoryTheory.Limits.PreservesColimit
                      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
                        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom))
                      (CategoryTheory.MonoidalCategory.tensorLeft X₁.right)] →
                  ((X₁ □ X₂) □ X₃) ≅ X₁ □ X₂ □ X₃
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- If two vector fields are `C^n` with `n ≥ m + 1`, then their Lie bracket is `C^m`.  -/
ContMDiffWithinAt.mlieBracketWithin_vectorField : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I (minSmoothness 𝕜 2) M]
  [CompleteSpace E] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] {m : WithTop ℕ∞} {U V : (x : M) → TangentSpace I x}
  {s : Set M} {x : M},
  ContMDiffWithinAt I I.tangent n (fun x => ⟨x, U x⟩) s x →
    ContMDiffWithinAt I I.tangent n (fun x => ⟨x, V x⟩) s x →
      UniqueMDiff[s] →
        x ∈ s →
          minSmoothness 𝕜 (m + 1) ≤ n →
            ContMDiffWithinAt I I.tangent m (fun x₀ => ⟨x₀, VectorField.mlieBracketWithin I U V s x₀⟩) s x
-- Lean.Elab.PreDefinition.EqnsUtils
/-- Try to close goal using `rfl` with smart unfolding turned off.  -/
Lean.Elab.Eqns.tryURefl : Lean.MVarId → Lean.MetaM Bool
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.grindTraceToGrind : Lean.TSyntax `tactic → Lean.Elab.Tactic.TacticM (Lean.TSyntax `tactic)
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- `mapAlg` is the morphism induced by `R → S`.  -/
Polynomial.mapAlg_eq_map : ∀ {R : Type u} [inst : CommSemiring R] (S : Type v) [inst_1 : Semiring S] [inst_2 : Algebra R S] (p : Polynomial R),
  (Polynomial.mapAlg R S) p = Polynomial.map (algebraMap R S) p
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- Eta-expanded form of `UniformContinuous.inv₀` -/
UniformContinuous.fun_inv₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} [inst_1 : UniformSpace X] {f : X → α},
  UniformContinuous f → (Set.range f)ᶜ ∈ nhds 0 → UniformContinuous fun i => (f i)⁻¹
-- Mathlib.RingTheory.Ideal.Int
Int.absNorm_under_mem : ∀ {R : Type u_1} [inst : Ring R] (I : Ideal R), ↑(Ideal.absNorm (Ideal.under ℤ I)) ∈ I
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a non-degenerate right-angled triangle is less than `π / 2`.  -/
InnerProductGeometry.angle_add_lt_pi_div_two_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x ≠ 0 → InnerProductGeometry.angle x (x + y) < Real.pi / 2
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.natMul.sizeOf_spec : ∀ (k : ℕ) (a : Lean.Grind.Linarith.Expr), sizeOf (Lean.Grind.Linarith.Expr.natMul k a) = 1 + sizeOf k + sizeOf a
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.overEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (Y : CategoryTheory.Over X)
  (R : CategoryTheory.Sieve Y),
  (CategoryTheory.Sieve.overEquiv Y) R = CategoryTheory.Sieve.functorPushforward (CategoryTheory.Over.forget X) R
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Ico_left_eq_Ico_sub_one : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] {a b : α} [NoMinOrder α],
  a ≤ b → insert (a - 1) (Set.Ico a b) = Set.Ico (a - 1) b
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- **Alias** of `UpperHalfPlane.ne_natCast`. -/
UpperHalfPlane.ne_nat : ∀ (z : UpperHalfPlane) (n : ℕ), ↑z ≠ ↑n
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticWithinAt.inv`

---

`(f x)⁻¹` is analytic away from `f x = 0`  -/
AnalyticWithinAt.fun_inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {x : E} {s : Set E}, AnalyticWithinAt 𝕜 f s x → f x ≠ 0 → AnalyticWithinAt 𝕜 (fun i => (f i)⁻¹) s x
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- **Alias** of `ChartedSpace.locallyPathConnectedSpace`.

---

If a topological space `M` admits an atlas with locally path-connected charts,
then `M` itself is locally path-connected.  -/
ChartedSpace.locPathConnectedSpace : ∀ (H : Type u) (M : Type u_2) [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [ChartedSpace H M]
  [LocallyPathConnectedSpace H], LocallyPathConnectedSpace M
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Set of E-matching theorems.  -/
Lean.Meta.Grind.EMatchTheorems : Type
-- Mathlib.RingTheory.Adjoin.Tower
Algebra.adjoin_restrictScalars : ∀ (C : Type u_1) (D : Type u_2) (E : Type u_3) [inst : CommSemiring C] [inst_1 : CommSemiring D]
  [inst_2 : CommSemiring E] [inst_3 : Algebra C D] [inst_4 : Algebra C E] [inst_5 : Algebra D E]
  [inst_6 : IsScalarTower C D E] (S : Set E),
  Subalgebra.restrictScalars C (Algebra.adjoin D S) =
    Subalgebra.restrictScalars C (Algebra.adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) S)
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.ofReal_normSq_eq_inner_self : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x : F), ↑(InnerProductSpace.Core.normSq x) = inner 𝕜 x x
-- Mathlib.Analysis.Convex.Function
concaveOn_iff_pairwise_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 β] {s : Set E}
  {f : E → β},
  ConcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.freeOn_isNonloop_iff : ∀ {α : Type u_1} {e : α} {E : Set α}, (Matroid.freeOn E).IsNonloop e ↔ e ∈ E
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instEpiSheafAddCommGrpCatGShortComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  (S : J.MayerVietorisSquare), CategoryTheory.Epi S.shortComplex.g
-- Init.Data.UInt.Lemmas
USize.toUInt32_toUInt8 : ∀ (n : USize), n.toUInt8.toUInt32 = n.toUInt32 % 256
-- Mathlib.Data.Set.Basic
Set.lt_iff_ssubset : ∀ {α : Type u} {s t : Set α}, s ⊂ t ↔ s ⊂ t
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_surjective : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀),
  Function.Surjective (WithVal.toVal v)
-- Mathlib.Tactic.SetNotationForOrder
/-- Elaborator for `x ⊃ y` notation.  -/
Mathlib.Meta.SetNotationForOrder.elabSSupsetStx' : Lean.Elab.Term.TermElab
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associator_naturality_left : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h)
      (CategoryTheory.Bicategory.associator f' g h).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom
      (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h))
-- Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
CategoryTheory.Limits.ι_sigmaConstCokernelCofork_π_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (R : C)
  {α : Type u_1} {β : Type u_2} (f : α → β) [inst_2 : CategoryTheory.Limits.HasCoproduct fun x => R]
  [inst_3 : CategoryTheory.Limits.HasCoproduct fun x => R] [inst_4 : CategoryTheory.Limits.HasCoproduct fun x => R]
  (a : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => R) (f a))
      (CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.sigmaConstCokernelCofork R f)) =
    0
-- Mathlib.Computability.DFA
DFA.comap_reindex : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) {α' : Type u_1} {σ' : Type u_2} (f : α' → α) (g : σ ≃ σ'),
  DFA.comap f ((DFA.reindex g) M) = (DFA.reindex g) (DFA.comap f M)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
/-- At `s = 0`, the Gamma function has a simple pole with residue 1.  -/
Complex.tendsto_self_mul_Gamma_nhds_zero : Filter.Tendsto (fun z => z * Complex.Gamma z) (nhdsWithin 0 {0}ᶜ) (nhds 1)
-- Mathlib.Order.CompleteLattice.Finset
Finset.iInf_biUnion : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CompleteLattice β] [inst_1 : DecidableEq α] (s : Finset γ)
  (t : γ → Finset α) (f : α → β), ⨅ y ∈ s.biUnion t, f y = ⨅ x ∈ s, ⨅ y ∈ t x, f y
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.toBornology : {α : Type u} → [self : PseudoMetricSpace α] → Bornology α
-- Mathlib.LinearAlgebra.Prod
Submodule.fst_sup_snd : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], Submodule.fst R M M₂ ⊔ Submodule.snd R M M₂ = ⊤
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
Filter.Subsingleton.atBot_eq : ∀ (α : Type u_6) [Subsingleton α] [inst : Preorder α], Filter.atBot = ⊤
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.supp_eq_valuation_supp : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : ValuativeRel R], ValuativeRel.supp R = (ValuativeRel.valuation R).supp
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- An oriented angle has a sign zero if and only if the three points are collinear.  -/
EuclideanGeometry.oangle_sign_eq_zero_iff_collinear : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign = 0 ↔ Collinear ℝ {p₁, p₂, p₃}
-- Mathlib.Data.Int.Init
/-- A strong recursor for `Int` that specifies explicit values for integers below a threshold,
and is analogous to `Nat.strongRec` for integers on or above the threshold.  -/
Int.strongRec : {m : ℤ} →
  {motive : ℤ → Sort u_1} →
    ((n : ℤ) → n < m → motive n) → ((n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n) → (n : ℤ) → motive n
-- Std.Sync.CancellationToken
Std.CancellationToken.Consumer.resolve : Std.CancellationToken.Consumer → BaseIO Bool
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_eq_bot : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [NoZeroDivisors A] {M N : Submodule R A}, M * N = ⊥ ↔ M = ⊥ ∨ N = ⊥
-- Mathlib.Order.Interval.Set.ProjIcc
Set.OrdConnected.IciExtend : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α} {s : Set ↑(Set.Ici a)},
  s.OrdConnected → {x | Set.IciExtend (fun x => x ∈ s) x}.OrdConnected
-- Mathlib.Data.List.Destutter
List.destutter'_cons_neg : ∀ {α : Type u_1} (l : List α) {R : α → α → Prop} [inst : DecidableRel R] {a b : α},
  ¬R b a → List.destutter' R b (a :: l) = List.destutter' R b l
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.of_carrier : ∀ (R : SemiRingCat), SemiRingCat.of ↑R = R
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.const_mul : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν →
    ∀ (r : ℝ), ProbabilityTheory.Kernel.HasSubgaussianMGF (fun ω => r * X ω) (NNReal.mk (r ^ 2) ⋯ * c) κ ν
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.unit_app : ∀ (P : TopCat → Prop) [inst : CompHausLike.HasProp P PUnit.{u + 1}]
  [inst_1 : CompHausLike.HasExplicitFiniteCoproducts P] [inst_2 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  (x : Type (max u u_1)),
  (CompHausLike.LocallyConstant.unit P hs).app x =
    TypeCat.ofHom fun x_1 => LocallyConstant.const (↑(CompHausLike.of P PUnit.{u + 1}).toTop) x_1
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.hasEigenvalue_of_hasEigenvector : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {x : M}, f.HasEigenvector μ x → f.HasEigenvalue μ
-- Lean.Parser.Types
/-- Returns the next position in the input string after position `p`. The result is unspecified if `p`
is not a valid position.

Requires evidence, `h`, that `p` is within bounds. No run-time bounds check is performed.
 -/
Lean.Parser.InputContext.next' : (c : Lean.Parser.InputContext) → (p : String.Pos.Raw) → ¬c.atEnd p = true → String.Pos.Raw
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.map_eq_top_iff : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {I : Ideal R},
  Function.Injective ⇑f → f.IsIntegral → (Ideal.map f I = ⊤ ↔ I = ⊤)
-- Mathlib.Algebra.Group.Irreducible.Lemmas
irreducible_units_mul : ∀ {M : Type u_2} [inst : Monoid M] {y : M} (u : Mˣ), Irreducible (↑u * y) ↔ Irreducible y
-- Mathlib.Probability.Moments.MGFAnalytic
/-- For `t ∈ interior (integrableExpSet X μ)`, the derivative of `mgf X μ` at `t` is
`μ[X * exp (t * X)]`.  -/
ProbabilityTheory.deriv_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    deriv (ProbabilityTheory.mgf X μ) t = ∫ (x : Ω), (fun ω => X ω * Real.exp (t * X ω)) x ∂μ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_union_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ ∪ t₂ ↔ k ∈ t₁ ∨ k ∈ t₂
-- Mathlib.Algebra.Group.Action.End
Function.End.one_def : ∀ {α : Type u_5}, 1 = id
-- Init.Data.List.Find
List.find?_eq_bind_findIdx?_getElem? : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, List.find? p xs = (List.findIdx? p xs).bind fun x => xs[x]?
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- The Fourier integral of the Fréchet derivative of a function is obtained by multiplying the
Fourier integral of the original function by `2πI x`.  -/
Real.fourier_deriv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E},
  MeasureTheory.Integrable f MeasureTheory.volume →
    Differentiable ℝ f →
      MeasureTheory.Integrable (deriv f) MeasureTheory.volume →
        FourierTransform.fourier (deriv f) = fun x => (2 * ↑Real.pi * Complex.I * ↑x) • FourierTransform.fourier f x
-- Mathlib.Algebra.Ring.NonZeroDivisors
mul_cancel_right_mem_nonZeroDivisors : ∀ {R : Type u_1} [inst : Ring R] {x y r : R}, r ∈ nonZeroDivisors R → (x * r = y * r ↔ x = y)
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roc.length_iter : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] [inst_6 : Std.Rxc.HasSize α] [Std.Rxc.LawfulHasSize α] {r : Std.Roc α},
  r.iter.length = r.size
-- Lean.Util.LeanOptions
Lean.LeanOptionValue.ofBool.inj : ∀ {b b_1 : Bool}, Lean.LeanOptionValue.ofBool b = Lean.LeanOptionValue.ofBool b_1 → b = b_1
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientMulEquivQuotientProd_snd : ∀ {R : Type u_2} [inst : CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I * J),
  ((I.quotientMulEquivQuotientProd J coprime) x).2 = (Ideal.Quotient.factor ⋯) x
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.ennreal_smul_eq_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {c : ENNReal} {μ : MeasureTheory.Measure α}, c • μ = 0 ↔ c = 0 ∨ μ = 0
-- Mathlib.Data.NNReal.Basic
NNReal.coe_indicator : ∀ {α : Type u_2} (s : Set α) (f : α → NNReal) (a : α), ↑(s.indicator f a) = s.indicator (fun x => ↑(f x)) a
-- Lean.Linter.Deprecated
Lean.Linter.checkDeprecated : Lean.Name → Lean.MetaM Unit
-- Mathlib.Analysis.Complex.Exponential
Real.exp_injective : Function.Injective Real.exp
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.centroid_restrict : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [CharZero k] {n : ℕ} (s : Affine.Simplex k P n) (S : AffineSubspace k P)
  (hS : affineSpan k (Set.range s.points) ≤ S), ↑(s.restrict S hS).centroid = s.centroid
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Creates the continued fraction of a value.  -/
ContFract.of : {K : Type u_1} → K → [inst : Field K] → [inst_1 : LinearOrder K] → [IsStrictOrderedRing K] → [FloorRing K] → ContFract K
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections],
  Small.{u, max u v}
    ↑((F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)).comp (CategoryTheory.forget AddMonCat)).sections
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- First projection from the intersection of two pre-`0`-hypercovers.  -/
CategoryTheory.PreZeroHypercover.interFst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (E : CategoryTheory.PreZeroHypercover S) →
        (F : CategoryTheory.PreZeroHypercover S) →
          [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] → (E.inter F).Hom E
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_add_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddGroup α] {t : Finset α} {a : α},
  Finset.image (fun b => a + b) t = t.preimage (fun b => -a + b) ⋯
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiff : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C),
  (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
-- Mathlib.Computability.Primrec.Basic
Primrec.option_map : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → Option β} {g : α → β → σ}, Primrec f → Primrec₂ g → Primrec fun a => Option.map (g a) (f a)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Definability
IsSemilinearSet.definable : ∀ {α : Type u_1} {s : Set (α → ℕ)} {A : Set ℕ} [Finite α],
  IsSemilinearSet s → A.Definable FirstOrder.Language.presburger s
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.allDiffAuxAux : {α : Type u} → [BEq α] → (as : Array α) → α → (i : ℕ) → i < as.size → Bool
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_re_add_im : ∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6} [inst_1 : RCLike 𝕜]
  {f : X → 𝕜},
  MeasureTheory.Integrable f μ →
    ↑(∫ (x : X), RCLike.re (f x) ∂μ) + ↑(∫ (x : X), RCLike.im (f x) ∂μ) * RCLike.I = ∫ (x : X), f x ∂μ
-- Batteries.Data.Array.Basic
/-- auxiliary tail-recursive function for scanrM  -/
Array.scanrM.loop : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_1} →
      [Monad m] → (α → β → m β) → β → (as : Array α) → (start : ℕ) → ℕ → start ≤ as.size → Array β → m (Array β)
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.empty_add_empty : ∀ {α : Type u_1} [inst : Add α] (v w : Fin 0 → α), v + w = ![]
-- Init.Data.Fin.Lemmas
Fin.castLE_comp_castLE : ∀ {k m n : ℕ} (km : k ≤ m) (mn : m ≤ n), Fin.castLE mn ∘ Fin.castLE km = Fin.castLE ⋯
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol.brecOn_4.go : {motive_1 : Lean.Lsp.DocumentSymbol → Sort u} →
  {motive_2 : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol → Sort u} →
    {motive_3 : Option (Array Lean.Lsp.DocumentSymbol) → Sort u} →
      {motive_4 : Array Lean.Lsp.DocumentSymbol → Sort u} →
        {motive_5 : List Lean.Lsp.DocumentSymbol → Sort u} →
          (t : List Lean.Lsp.DocumentSymbol) →
            ((t : Lean.Lsp.DocumentSymbol) → t.below → motive_1 t) →
              ((t : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol) →
                  Lean.Lsp.DocumentSymbol.below_1 t → motive_2 t) →
                ((t : Option (Array Lean.Lsp.DocumentSymbol)) → Lean.Lsp.DocumentSymbol.below_2 t → motive_3 t) →
                  ((t : Array Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_3 t → motive_4 t) →
                    ((t : List Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_4 t → motive_5 t) →
                      motive_5 t ×' Lean.Lsp.DocumentSymbol.below_4 t
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
SimpleGraph.interedges.eq_1 : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] (s t : Finset α),
  G.interedges s t = Rel.interedges G.Adj s t
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The inner product of two vectors is the product of the norms and the cosine of the oriented
angle between the vectors.  -/
Orientation.inner_eq_norm_mul_norm_mul_cos_oangle : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), inner ℝ x y = ‖x‖ * ‖y‖ * (o.oangle x y).cos
-- Mathlib.Order.Partition.Basic
/-- Any partially defined representative function extends to a complete one.  -/
Partition.IsRepFun.exists_extend_partial : ∀ {α : Type u_1} {t u : Set α} (P : Partition u) (f₀ : ↑t → α),
  (∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x) →
    (∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)) →
      (∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y) → ∃ f, P.IsRepFun f ∧ ∀ (x : ↑t), f ↑x = f₀ x
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a cocone on `F : Jᵒᵖ ⥤ C` to a cone on `F.rightOp : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.coneRightOpOfCocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor Jᵒᵖ C} → CategoryTheory.Limits.Cocone F → CategoryTheory.Limits.Cone F.rightOp