mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Equiv.Defs
/-- An additive equivalence of additive groups preserves subtractions.  -/
AddEquiv.map_sub : ∀ {G : Type u_7} {H : Type u_8} [inst : AddGroup G] [inst_1 : SubtractionMonoid H] (h : G ≃+ H) (x y : G),
  h (x - y) = h x - h y
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivary_neg_left`. -/
Antivary.of_neg_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Antivary (-f) g → Monovary f g
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.instLawfulSingletonSigma : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α],
  LawfulSingleton ((a : α) × β a) (Std.DHashMap.Raw α β)
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
/-- The epimorphism from `p` of this presentation  -/
CategoryTheory.ProjectivePresentation.f : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X : C} → (self : CategoryTheory.ProjectivePresentation X) → self.p ⟶ X
-- Init.GrindInstances.ToInt
Int64.size.eq_1 : Int64.size = 18446744073709551616
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.equiv_iff_toArray_perm : ∀ {α : Type u} {β : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β}, t₁.Equiv t₂ ↔ t₁.toArray.Perm t₂.toArray
-- Mathlib.Analysis.Complex.Exponential
Complex.norm_exp_sub_sum_le_norm_mul_exp : ∀ (x : ℂ) (n : ℕ), ‖Complex.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial‖ ≤ ‖x‖ ^ n * Real.exp ‖x‖
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.Measure.withDensityᵥ.eq_1 : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (f : α → E),
  μ.withDensityᵥ f =
    if hf : MeasureTheory.Integrable f μ then
      { measureOf' := fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯, not_measurable' := ⋯,
        m_iUnion' := ⋯ }
    else 0
-- Mathlib.AlgebraicTopology.DoldKan.Projections
/-- All the `P q` coincide with `𝟙 _` in degree 0.  -/
AlgebraicTopology.DoldKan.P_f_0_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q : ℕ),
  (AlgebraicTopology.DoldKan.P q).f 0 =
    CategoryTheory.CategoryStruct.id ((AlgebraicTopology.AlternatingFaceMapComplex.obj X).X 0)
-- Mathlib.Combinatorics.SimpleGraph.Prod
/-- Project a walk on `G □ H` to a walk on `G` by discarding the moves in the direction of `H`.  -/
SimpleGraph.Walk.ofBoxProdLeft : {α : Type u_1} →
  {β : Type u_2} →
    {G : SimpleGraph α} →
      {H : SimpleGraph β} → [DecidableEq β] → [DecidableRel G.Adj] → {x y : α × β} → (G □ H).Walk x y → G.Walk x.1 y.1
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.touchpoint_mem_exsphere : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs → ∀ (i : Fin (n + 1)), s.touchpoint signs i ∈ s.exsphere signs
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.mulC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ : Lean.Grind.CommRing.Poly) (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.mul_certC p₁ k p c = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ = 0 → Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.μ_hom : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X Y : Action (Type u) G},
  Rep.Hom.hom (CategoryTheory.Functor.LaxMonoidal.μ (Rep.linearization k G) X Y) =
    Representation.LinearizeMonoidal.μ X Y
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.IsWeakLimit.mk.inj : ∀ {J : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} J} {C : Type u_3}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} C} {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
  {lift : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt}
  {fac :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (j : J),
        CategoryTheory.CategoryStruct.comp (lift s) (t.π.app j) = s.π.app j)
      CategoryTheory.Limits.IsWeakLimit.fac._autoParam}
  {lift_1 : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt}
  {fac_1 :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (j : J),
        CategoryTheory.CategoryStruct.comp (lift_1 s) (t.π.app j) = s.π.app j)
      CategoryTheory.Limits.IsWeakLimit.fac._autoParam},
  { lift := lift, fac := fac } = { lift := lift_1, fac := fac_1 } → lift = lift_1
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm_comm : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (x y : L),
  ((LieModule.traceForm R L M) x) y = ((LieModule.traceForm R L M) y) x
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- **Alias** of `Asymptotics.IsEquivalent.summable_iff_nat`. -/
IsEquivalent.summable_iff_nat : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {f g : ℕ → E},
  Asymptotics.IsEquivalent Filter.atTop f g → (Summable f ↔ Summable g)
-- Std.Sat.AIG.LawfulVecOperator
Std.Sat.AIG.LawfulVecOperator.mk : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → ℕ → Type}
  {f : {len : ℕ} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len},
  (∀ {len : ℕ} (aig : Std.Sat.AIG α) (input : β aig len), aig.decls.size ≤ (f aig input).aig.decls.size) →
    (∀ {len : ℕ} (aig : Std.Sat.AIG α) (input : β aig len) (idx : ℕ) (h1 : idx < aig.decls.size)
        (h2 : idx < (f aig input).aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]) →
      Std.Sat.AIG.LawfulVecOperator α β f
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.homOfLe_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  {G G' : CategoryTheory.Subfunctor F} (h : G ≤ G') (U : C),
  (CategoryTheory.Subfunctor.homOfLe h).app U = TypeCat.ofHom fun x => ⟨↑x, ⋯⟩
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mrange_inl_sup_mrange_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.mrange (MonoidHom.inl M N) ⊔ MonoidHom.mrange (MonoidHom.inr M N) = ⊤
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Inner
Measurable.const_inner : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {x : MeasurableSpace α} [inst_3 : MeasurableSpace E] [OpensMeasurableSpace E]
  [SecondCountableTopology E] {c : E} {f : α → E}, Measurable f → Measurable fun t => inner 𝕜 c (f t)
-- Mathlib.Topology.FiberBundle.Trivialization
OpenPartialHomeomorph.IsImage.restr.congr_simp : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e e_1 : OpenPartialHomeomorph X Y} (e_e : e = e_1) {s s_1 : Set X} (e_s : s = s_1) {t t_1 : Set Y} (e_t : t = t_1)
  (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)), h.restr hs = ⋯.restr ⋯
-- Init.Data.Format.Basic
/-- Determines how groups should have linebreaks inserted when the text would overfill its remaining
space.

- `allOrNone` will make a linebreak on every `Format.line` in the group or none of them.
  ```
  [1,
   2,
   3]
  ```
- `fill` will only make linebreaks on as few `Format.line`s as possible:
  ```
  [1, 2,
   3]
  ```
 -/
Std.Format.FlattenBehavior : Type
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraComplex.ofComplex_I : CliffordAlgebraComplex.ofComplex Complex.I = (CliffordAlgebra.ι CliffordAlgebraComplex.Q) 1
-- Init.Data.List.Nat.Range
List.drop_range' : ∀ {start n step k : ℕ}, List.drop k (List.range' start n step) = List.range' (start + k * step) (n - k) step
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.toLin'_symm_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (A : Matrix.SpecialLinearGroup n R) (v : n → R), (Matrix.SpecialLinearGroup.toLin' A).symm v = (Matrix.toLin' ↑A⁻¹) v
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.module : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → {N : LieSubmodule R L M} → Module R (M ⧸ N)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ),
  (Set.range τ).Countable → ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
-- Lean.Elab.DefView
Lean.Elab.DefView.mk : Lean.Elab.DefKind →
  Lean.Syntax →
    Lean.Syntax →
      Lean.Elab.Modifiers →
        Lean.Syntax →
          Lean.Syntax →
            Option Lean.Syntax →
              Lean.Syntax →
                Option (Lean.TSyntax `Lean.Parser.Command.docComment) →
                  Option (Lean.Language.SnapshotBundle (Option Lean.Elab.HeaderProcessedSnapshot)) →
                    Option (Array Lean.Syntax) → Lean.Elab.DefView
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- Given `X : CofibrantObject C`, this is a trivial cofibration
from `X` to a choice of bifibrant resolution.  -/
HomotopicalAlgebra.CofibrantObject.iBifibrantResolutionObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      (X : HomotopicalAlgebra.CofibrantObject C) →
        X ⟶ HomotopicalAlgebra.BifibrantObject.ιCofibrantObject.obj X.bifibrantResolutionObj
-- Aesop.Forward.Match.Types
Aesop.Match.mk : Aesop.Substitution →
  Array Aesop.Substitution → Aesop.SlotIndex → Array Aesop.PremiseIndex → Array Aesop.PremiseIndex → Aesop.Match
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_lift : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor K D}
  (h : CategoryTheory.Limits.Cone G ≌ CategoryTheory.Limits.Cone F) {c : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Limits.IsLimit.ofConeEquiv h).symm P).lift s =
    CategoryTheory.CategoryStruct.comp (h.counitIso.inv.app s).hom
      (h.functor.map (P.liftConeMorphism (h.inverse.obj s))).hom
-- Mathlib.Data.FinEnum
/-- enumerate all finite sets of a given type  -/
FinEnum.Finset.enum : {α : Type u} → [DecidableEq α] → List α → List (Finset α)
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_rpow : ∀ {a b r : ℝ}, -1 < r ∨ r ≠ -1 ∧ 0 ∉ Set.uIcc a b → ∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.unopHom_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (X Y : Cᵒᵖ)
  (f : X ⟶ Y), (CategoryTheory.unopHom X Y) f = f.unop
-- Mathlib.Analysis.Seminorm
Seminorm.mk.injEq : ∀ {𝕜 : Type u_12} {E : Type u_13} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E]
  (toAddGroupSeminorm : AddGroupSeminorm E)
  (smul' : ∀ (a : 𝕜) (x : E), toAddGroupSeminorm.toFun (a • x) = ‖a‖ * toAddGroupSeminorm.toFun x)
  (toAddGroupSeminorm_1 : AddGroupSeminorm E)
  (smul'_1 : ∀ (a : 𝕜) (x : E), toAddGroupSeminorm_1.toFun (a • x) = ‖a‖ * toAddGroupSeminorm_1.toFun x),
  ({ toAddGroupSeminorm := toAddGroupSeminorm, smul' := smul' } =
      { toAddGroupSeminorm := toAddGroupSeminorm_1, smul' := smul'_1 }) =
    (toAddGroupSeminorm = toAddGroupSeminorm_1)
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.struct.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preregular C]
  [inst_2 : CategoryTheory.FinitaryExtensive C]
  {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))}
  [inst_3 : SizeOf C] (X : ℕ → C) (x : (n : ℕ) → (F.obj (Opposite.op n)).obj.obj (Opposite.op (X n)))
  (map : (n : ℕ) → X (n + 1) ⟶ X n) (effectiveEpi : ∀ (n : ℕ), CategoryTheory.EffectiveEpi (map n))
  (w :
    ∀ (n : ℕ),
      (CategoryTheory.ConcreteCategory.hom ((F.map (CategoryTheory.homOfLE ⋯).op).hom.app (Opposite.op (X (n + 1)))))
          (x (n + 1)) =
        (CategoryTheory.ConcreteCategory.hom ((F.obj (Opposite.op n)).obj.map (map n).op)) (x n)),
  sizeOf { X := X, x := x, map := map, effectiveEpi := effectiveEpi, w := w } = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- A cokernel cofork is just a cofork where the second morphism is a zero morphism.  -/
CategoryTheory.Limits.CokernelCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] → {X Y : C} → (X ⟶ Y) → Type (max u v)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_le_card_add_left : ∀ {α : Type u_2} [inst : Add α] [IsLeftCancelAdd α] [inst_2 : DecidableEq α] {t s : Finset α},
  s.Nonempty → t.card ≤ (s + t).card
-- Mathlib.Topology.MetricSpace.Thickening
Metric.ediam_thickening_le : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α} (ε : NNReal),
  Metric.ediam (Metric.thickening (↑ε) s) ≤ Metric.ediam s + 2 * ↑ε
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.integral_prod_bilin : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {E : Type u_5} {F : Type u_6}
  {G : Type u_7} {𝕜 : Type u_8} [inst_4 : RCLike 𝕜] [inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace ℝ E]
  [inst_7 : NormedSpace 𝕜 E] [CompleteSpace E] [inst_9 : NormedAddCommGroup F] [inst_10 : NormedSpace ℝ F]
  [inst_11 : NormedSpace 𝕜 F] [CompleteSpace F] [inst_13 : NormedAddCommGroup G] [inst_14 : NormedSpace ℝ G]
  [inst_15 : NormedSpace 𝕜 G] [CompleteSpace G] (B : E →L[𝕜] F →L[𝕜] G) {f : α → E} {g : β → F},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g ν →
      ∫ (z : α × β), (B (f z.1)) (g z.2) ∂μ.prod ν = (B (∫ (x : α), f x ∂μ)) (∫ (y : β), g y ∂ν)
-- Mathlib.Algebra.Order.Archimedean.Real.Hom
Real.ringHom_apply : ∀ {F : Type u_1} [inst : FunLike F ℝ ℝ] [RingHomClass F ℝ ℝ] (f : F) (r : ℝ), f r = r
-- Init.Data.Vector.Attach
/-- This lemma identifies folds over arrays of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
Vector.foldl_subtype : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {p : α → Prop} {xs : Vector { x // p x } n} {f : β → { x // p x } → β}
  {g : β → α → β} {x : β},
  (∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x) → Vector.foldl f x xs = Vector.foldl g x xs.unattach
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
InnerProductGeometry.angle.eq_1 : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  InnerProductGeometry.angle x y = Real.arccos (inner ℝ x y / (‖x‖ * ‖y‖))
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.forget_map : ∀ {X Y : AddMonCat} (f : X ⟶ Y),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget AddMonCat).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instMax : {α : Type u_1} → [inst : TopologicalSpace α] → Max (TopologicalSpace.Compacts α)
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
/-- `ENNReal.log` and its inverse `EReal.exp` are an order isomorphism between `ℝ≥0∞` and
`EReal`.  -/
ENNReal.logOrderIso : ENNReal ≃o EReal
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- A general inner product implies a real inner product. This is not registered as an instance
since `𝕜` does not appear in the return type `Inner ℝ E`.  -/
Inner.rclikeToReal : (𝕜 : Type u_1) →
  (E : Type u_2) → [inst : RCLike 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → Inner ℝ E
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_zero : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}, ProbabilityTheory.condVar m 0 μ = 0
-- Mathlib.Algebra.Group.Defs
mul_eq_one_comm : ∀ {M : Type u_2} [inst : MulOne M] [IsDedekindFiniteMonoid M] {a b : M}, a * b = 1 ↔ b * a = 1
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inrHom_apply : ∀ (S : Type u_2) (R : Type u_3) (A : Type u_4) [inst : Semiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid A]
  [inst_3 : Module S R] [inst_4 : Module S A] (a : A), (Unitization.inrHom S R A) a = ↑a
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.sum_vAddAntidiagonal_eq : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ]
  [inst_1 : PartialOrder Γ'] [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid R] [inst_4 : SMulWithZero R V]
  [inst_5 : VAdd Γ Γ'] [inst_6 : IsOrderedCancelVAdd Γ Γ'] (s : HahnSeries.SummableFamily Γ R α)
  (t : HahnSeries.SummableFamily Γ' V β) (g : Γ') (a : α × β),
  ∑ x ∈ Finset.VAddAntidiagonal g ⋯, (s a.1).coeff x.1 • (t a.2).coeff x.2 =
    ∑ x ∈ Finset.VAddAntidiagonal g ⋯, (s a.1).coeff x.1 • (t a.2).coeff x.2
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons_eq_cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp1 exp2 : ℝ}
  {coef1 coef2 : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl1 tl2 : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp1 coef1 tl1 =
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp2 coef2 tl2 ↔
    exp1 = exp2 ∧ coef1 = coef2 ∧ tl1 = tl2
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
borel_eq_generateFrom_Ioc_le : ∀ (α : Type u_5) [inst : TopologicalSpace α] [SecondCountableTopology α] [inst_2 : LinearOrder α] [OrderTopology α],
  borel α = MeasurableSpace.generateFrom {S | ∃ l u, l ≤ u ∧ Set.Ioc l u = S}
-- Mathlib.CategoryTheory.Functor.Const
CategoryTheory.Functor.const_obj_obj : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : C) (x : J), ((CategoryTheory.Functor.const J).obj X).obj x = X
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {f : (a : α) → β a → γ a} {k : α},
  (Std.ExtDHashMap.map f m).getKey! k = m.getKey! k
-- Mathlib.CategoryTheory.Category.Pointed
/-- `typeToPointed` is the free functor.  -/
typeToPointedForgetAdjunction : typeToPointed ⊣ CategoryTheory.forget Pointed
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isPullback : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰)
  [∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.Limits.PreservesColimitsOfShape J
        (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
  {i j : 𝒰.I₀} (hij : i ⟶ j),
  CategoryTheory.IsPullback (d.transitionMap hij).left (d.cocone i).pt.hom (d.cocone j).pt.hom
    (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij)
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
_private.Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes.0.CategoryTheory.Functor.homObjEquiv.match_1.eq_1 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] (F A : CategoryTheory.Functor C (Type u_2)) (X : C)
  (motive : (CategoryTheory.MonoidalCategoryStruct.tensorObj F A).obj X → Sort u_4) (x : F.obj X) (y : A.obj X)
  (h_1 : (x : F.obj X) → (y : A.obj X) → motive (x, y)),
  (match (x, y) with
    | (x, y) => h_1 x y) =
    h_1 x y
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rio_one_eq_singleton : (*...1).toArray = #[0]
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.zeroLocus_iUnion : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} {ι : Type u_1} (f : ι → Set ↑(X.presheaf.obj (Opposite.op U))),
  X.zeroLocus (⋃ i, f i) = ⋂ i, X.zeroLocus (f i)
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_finsetSum : ∀ {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} (mΩ : MeasurableSpace Ω)
  (s : Finset ι) {X : ι → Ω → ENNReal},
  (∀ (i : ι), AEMeasurable (X i) P) → P⁻[∑ i ∈ s, X i | mΩ] =ᵐ[P] ∑ i ∈ s, P⁻[X i | mΩ]
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapAlgEquiv_trans : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {C : Type u_6} {M : Type u_7} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Algebra R C] [inst_7 : Monoid M] (e₁ : A ≃ₐ[R] B) (e₂ : B ≃ₐ[R] C),
  MonoidAlgebra.mapAlgEquiv R M (e₁.trans e₂) =
    (MonoidAlgebra.mapAlgEquiv R M e₁).trans (MonoidAlgebra.mapAlgEquiv R M e₂)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.eq_spanSingleton_of_principal : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] (I : FractionalIdeal S P) [inst_4 : (↑I).IsPrincipal],
  I = FractionalIdeal.spanSingleton S (Submodule.IsPrincipal.generator ↑I)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.checkPrec.formatter : Lean.PrettyPrinter.Formatter
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr : ∀ (n w : ℕ) (expr expr' : BitVec w), expr' = expr → BitVec.replicate n expr' = BitVec.replicate n expr
-- Lean.Level
Lean.Level.PP.Result.num.injEq : ∀ (a a_1 : ℕ), (Lean.Level.PP.Result.num a = Lean.Level.PP.Result.num a_1) = (a = a_1)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanImport : Lean.ToJson Lean.Lsp.LeanImport
-- Mathlib.Topology.MetricSpace.Thickening
Metric.mem_cthickening_of_edist_le : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x y : α) (δ : ℝ) (E : Set α),
  y ∈ E → edist x y ≤ ENNReal.ofReal δ → x ∈ Metric.cthickening δ E
-- Std.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_3.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterM m α → Sort u_3)
  (h_1 : Unit → motive { internalState := { list := [] } })
  (h_2 : (x : α) → (xs : List α) → motive { internalState := { list := x :: xs } }),
  (match { internalState := { list := [] } } with
    | { internalState := { list := [] } } => h_1 ()
    | { internalState := { list := x :: xs } } => h_2 x xs) =
    h_1 ()
-- Init.Data.BitVec.Lemmas
/-- `rotateRight` is defined in terms of left and right shifts.  -/
BitVec.rotateRight_def : ∀ {w : ℕ} {x : BitVec w} {r : ℕ}, x.rotateRight r = x >>> (r % w) ||| x <<< (w - r % w)