mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitUncurryIsoLimitCompLim_inv_π_assoc : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.uncurry.obj F)]
  [inst_5 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C}
  (h : (CategoryTheory.Functor.uncurry.obj F).obj (j, k) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.uncurry.obj F) (j, k))
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.obj j) k) h)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.leftIso_inv : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T}
  {R₁ : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L₁ R₁} (α : X ≅ Y),
  (CategoryTheory.Comma.leftIso α).inv = α.inv.left
-- Mathlib.Order.WithBot
/-- `WithBot.ofDual` is the equivalence sending `⊥` to `⊤` and any `a : αᵒᵈ` to `ofDual a : α`.
See `WithBot.ofDualTopEquiv` for the related order-iso.
 -/
WithBot.ofDual : {α : Type u_1} → WithBot αᵒᵈ ≃ WithTop α
-- Mathlib.Analysis.InnerProductSpace.LinearMap
LinearMap.isometryOfInner_toLinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E')
  (h : ∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y), (f.isometryOfInner h).toLinearMap = f
-- Std.Internal.UV.Signal
/-- This function has different behavior depending on the state of the `Signal`:
- If it is initial or finished this is a no-op.
- If it is running the signal handler is stopped and it is put into the finished state.
  Note that if the last `IO.Promise` generated by `next` is unresolved and being waited
  on this creates a memory leak and the waiting task is not going to be awoken anymore.
 -/
Std.Internal.UV.Signal.stop : Std.Internal.UV.Signal → IO Unit
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionList.mk.sizeOf_spec : ∀ (isIncomplete : Bool) (items : Array Lean.Lsp.ResolvableCompletionItem),
  sizeOf { isIncomplete := isIncomplete, items := items } = 1 + sizeOf isIncomplete + sizeOf items
-- Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
measurable_of_re_im : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace α] {f : α → 𝕜},
  (Measurable fun x => RCLike.re (f x)) → (Measurable fun x => RCLike.im (f x)) → Measurable f
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- Let `b` be a basis for `S` over `ℤ` and `bI` a basis for `I` over `ℤ` of the same dimension.
Then an alternative way to compute the norm of `I` is given by taking the determinant of `bI`
over `b`.  -/
Ideal.natAbs_det_basis_change : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  {ι : Type u_2} [inst_4 : Fintype ι] [inst_5 : DecidableEq ι] (b : Module.Basis ι ℤ S) (I : Ideal S)
  (bI : Module.Basis ι ℤ ↥I), (b.det (Subtype.val ∘ ⇑bI)).natAbs = Ideal.absNorm I
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Push forward an affine simplex under an injective affine map.  -/
Affine.Simplex.map : {k : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_3} →
      {P : Type u_5} →
        {P₂ : Type u_6} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V P] →
                      [inst_6 : AddTorsor V₂ P₂] →
                        {n : ℕ} →
                          Affine.Simplex k P n → (f : P →ᵃ[k] P₂) → Function.Injective ⇑f → Affine.Simplex k P₂ n
-- Mathlib.MeasureTheory.Measure.Prod
/-- If `μ`-a.e. section `{y | (x, y) ∈ s}` of a measurable set have `ν` measure zero,
then `s` has `μ.prod ν` measure zero.

This implication requires `s` to be measurable but does not require `ν` to be s-finite.
See also `measure_prod_null` and `measure_ae_null_of_prod_null` below.  -/
MeasureTheory.Measure.measure_prod_null_of_ae_null : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {s : Set (α × β)},
  MeasurableSet s → (fun x => ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0 → (μ.prod ν) s = 0
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.ins.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_3 ()
-- Mathlib.RepresentationTheory.Induced
Rep.coinvariantsTensorIndIso_hom : ∀ {k : Type u} [inst : CommRing k] {G H : Type u} [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  (A : Rep.{u, u, u} k G) (B : Rep.{u, u, u} k H),
  (Rep.coinvariantsTensorIndIso φ A B).hom = Rep.coinvariantsTensorIndHom φ A B
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  {e e' : F.RepresentableBy Y},
  e.homEquiv (CategoryTheory.CategoryStruct.id Y) = e'.homEquiv (CategoryTheory.CategoryStruct.id Y) → e = e'
-- Mathlib.RingTheory.FractionalIdeal.Basic
_private.Mathlib.RingTheory.FractionalIdeal.Basic.0.Nat.unaryCast.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_add_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddGroup α] {t : Finset α} {b : α},
  Finset.image (fun x => x + b) t = t.preimage (fun x => x + -b) ⋯
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (I₀ : Type w) (X : I₀ → C) (f : (i : I₀) → X i ⟶ S)
  (I₀_1 : Type w) (X_1 : I₀_1 → C) (f_1 : (i : I₀_1) → X_1 i ⟶ S),
  ({ I₀ := I₀, X := X, f := f } = { I₀ := I₀_1, X := X_1, f := f_1 }) = (I₀ = I₀_1 ∧ X ≍ X_1 ∧ f ≍ f_1)
-- Mathlib.Order.BoundedOrder.Basic
not_isMax_iff_lt_top : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] {a : α}, ¬IsMax a ↔ a < ⊤
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.ω_mul_h : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [CharZero R] [inst_7 : Fintype ι] (i : ↥b.support),
  RootPairing.GeckConstruction.ω b * RootPairing.GeckConstruction.h i =
    -RootPairing.GeckConstruction.h i * RootPairing.GeckConstruction.ω b
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_ofNat_of_lt : ∀ {n : ℕ}, n < 2 ^ 31 → (ISize.ofNat n).toNatClampNeg = n
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- All `HasMulAntidiagonal` instances are equal  -/
Finset.HasMulAntidiagonal.instSubsingleton : ∀ {A : Type u_1} [inst : Monoid A], Subsingleton (Finset.HasMulAntidiagonal A)
-- Init.Grind.AC
Lean.Grind.AC.Expr.op.sizeOf_spec : ∀ (lhs rhs : Lean.Grind.AC.Expr), sizeOf (lhs.op rhs) = 1 + sizeOf lhs + sizeOf rhs
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If a functor preserves equalizers and the appropriate products, it preserves limits.  -/
CategoryTheory.Limits.preservesLimit_of_preservesEqualizers_and_product : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C]
  [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) C]
  [CategoryTheory.Limits.HasEqualizers C] (G : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) G]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) G],
  CategoryTheory.Limits.PreservesLimitsOfShape J G
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.uniqueLinearEquiv.congr_simp : ∀ (R : Type u_1) {α : Type u_3} (M : Type u_4) [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M]
  [inst_3 : Subsingleton α] (a a_1 : α), a = a_1 → Finsupp.uniqueLinearEquiv R M a = Finsupp.uniqueLinearEquiv R M a_1
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.toJordanDecomposition_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α], MeasureTheory.SignedMeasure.toJordanDecomposition 0 = 0
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.functorCategoryHasColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  [∀ (k : K), CategoryTheory.Limits.HasColimit (F.flip.obj k)], CategoryTheory.Limits.HasColimit F
-- Mathlib.Algebra.Star.CentroidHom
CentroidHom.instStarAddMonoidCenter : {α : Type u_1} →
  [inst : NonUnitalNonAssocSemiring α] → [StarRing α] → StarAddMonoid ↥(Subsemiring.center (CentroidHom α))
-- Mathlib.Algebra.Group.Units.Hom
/-- Coercion `AddUnits M → M` as an AddMonoid homomorphism.  -/
AddUnits.coeHom : (M : Type u) → [inst : AddMonoid M] → AddUnits M →+ M
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.mk.injEq : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] (countdown : ℕ) (inner : Std.IterM m β)
  (finite : countdown > 0 ∨ Std.Iterators.Finite α m) (countdown_1 : ℕ) (inner_1 : Std.IterM m β)
  (finite_1 : countdown_1 > 0 ∨ Std.Iterators.Finite α m),
  ({ countdown := countdown, inner := inner, finite := finite } =
      { countdown := countdown_1, inner := inner_1, finite := finite_1 }) =
    (countdown = countdown_1 ∧ inner = inner_1)
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.familyOfElements.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j)
  {D₁ D₂ : F.DescentData f}
  (φ φ_1 :
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂),
  φ = φ_1 →
    ∀ (i : ι) ⦃Y : CategoryTheory.Over (X i)⦄
      (f_1 f_2 : Y ⟶ CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (X i))) (e_f : f_1 = f_2)
      (a : (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve✝ f f' i).arrows f_1),
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.familyOfElements✝ w φ i f_1 a =
        CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.familyOfElements✝ w φ_1 i f_2 ⋯
-- Init.Data.Range.Polymorphic.Fin
Fin.instLawfulUpwardEnumerableLE : ∀ {n : ℕ}, Std.PRange.LawfulUpwardEnumerableLE (Fin n)
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.congr_simp : ∀ (R : Type u_5) (E : Type u_6) [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E], PointedCone R E = PointedCone R E
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_self_add_right : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : AddGroup N] (f g : α →₀ N),
  f.neLocus (f + g) = g.support
-- Mathlib.Topology.Basic
IsOpen.and : ∀ {X : Type u} {p₁ p₂ : X → Prop} [inst : TopologicalSpace X],
  IsOpen {x | p₁ x} → IsOpen {x | p₂ x} → IsOpen {x | p₁ x ∧ p₂ x}
-- Mathlib.Topology.Category.Compactum
CompHaus.forgetCreatesLimits : CategoryTheory.CreatesLimits (CategoryTheory.forget CompHaus)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.tensorμ_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (W X Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ W X Y Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.snd (CategoryTheory.MonoidalCategoryStruct.tensorObj W Y)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.SemiCartesianMonoidalCategory.snd W X)
        (CategoryTheory.SemiCartesianMonoidalCategory.snd Y Z))
      h
-- Mathlib.RingTheory.Etale.StandardEtale
/-- The monic polynomial to be quotiented out in a standard etale algebra.  -/
StandardEtalePair.f : {R : Type u_1} → [inst : CommRing R] → StandardEtalePair R → Polynomial R
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f.op g.op)
      (CategoryTheory.Limits.pullbackIsoUnopPushout f g).hom.op =
    (CategoryTheory.Limits.pullback.fst f g).op
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isNegNNRat.sizeOf_spec : ∀ (inst : Lean.Expr) (q : ℚ) (n d proof : Lean.Expr),
  sizeOf (Mathlib.Meta.NormNum.Result'.isNegNNRat inst q n d proof) =
    1 + sizeOf inst + sizeOf q + sizeOf n + sizeOf d + sizeOf proof
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.throw_ReaderT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε : Type u_1}
  {α ρ : Type u} {epost : EPred} [inst_4 : MonadExceptOf ε m] (err : ε) (post : α → ρ → Pred),
  ⦃ Std.Internal.Do.wp (MonadLift.monadLift (MonadExceptOf.throw err)) post epost ⦄ MonadExceptOf.throw err ⦃ post;
    epost ⦄
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isoSpec.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U), hU.isoSpec = hU.isoSpec
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.Adj.right_triangle_components : ∀ {C₁ C₂ : CategoryTheory.Bicategory.Adj CategoryTheory.Cat} (α : C₁ ⟶ C₂) (X : ↑C₂.obj),
  CategoryTheory.CategoryStruct.comp (α.adj.unit.toNatTrans.app (α.r.toFunctor.obj X))
      (α.r.toFunctor.map (α.adj.counit.toNatTrans.app X)) =
    CategoryTheory.CategoryStruct.id (α.r.toFunctor.obj X)
-- Mathlib.Data.Fin.Tuple.Finset
Fin.mem_piFinset_iff_last_init : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} {f : (i : Fin (n + 1)) → α i} {s : (i : Fin (n + 1)) → Finset (α i)},
  f ∈ Fintype.piFinset s ↔ f (Fin.last n) ∈ s (Fin.last n) ∧ Fin.init f ∈ Fintype.piFinset (Fin.init s)
-- Mathlib.Algebra.BigOperators.Pi
Prod.fst_sum : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {s : Finset ι}
  {f : ι → M × N}, (∑ c ∈ s, f c).1 = ∑ c ∈ s, (f c).1
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.sec_spec' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  {f : S.LocalizationMap N} (z : N), f (f.sec z).1 = f ↑(f.sec z).2 + z
-- Mathlib.Algebra.GroupWithZero.Units.Basic
mul_div_cancel_of_imp : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, (b = 0 → a = 0) → a * b / b = a
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_natCast : ∀ {α : Type u_1} {n : Type u_4} [inst : Semiring α] [inst_1 : StarRing α] [inst_2 : DecidableEq n] (d : ℕ),
  (↑d).IsHermitian
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.id_comp : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} (f : B₁ →bᵢ B₂), (LinearMap.BilinForm.Isometry.id B₂).comp f = f
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.image_add_left_Ioo : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] [inst_5 : DecidableEq α] (a b c : α),
  Finset.image (fun x => c + x) (Finset.Ioo a b) = Finset.Ioo (c + a) (c + b)
-- Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
/-- `continuousMapPresheaf` as a presheaf of abelian groups associated to a topological abelian
group.  -/
AlgebraicGeometry.continuousMapPresheafAb : (A : Type v) →
  [inst : TopologicalSpace A] →
    [inst_1 : AddCommGroup A] → [IsTopologicalAddGroup A] → CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ Ab
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- The first morphism of a triangle, as a natural transformation `π₁ ⟶ π₂`.  -/
CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      CategoryTheory.Pretriangulated.Triangle.π₁ ⟶ CategoryTheory.Pretriangulated.Triangle.π₂
-- Mathlib.Analysis.Analytic.Order
/-- Characterization of which natural numbers are `≤ hf.order`. Useful for avoiding case splits,
since it applies whether or not the order is `∞`.  -/
natCast_le_analyticOrderAt : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜},
  AnalyticAt 𝕜 f z₀ →
    ∀ {n : ℕ}, ↑n ≤ analyticOrderAt f z₀ ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in nhds z₀, f z = (z - z₀) ^ n • g z
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} {h' : k ∈ Std.DTreeMap.filter f t},
  Std.DTreeMap.Const.get (Std.DTreeMap.filter f t) k h' = Std.DTreeMap.Const.get t k ⋯
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.induction : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] {C : DirectLimit F f → Prop},
  (∀ (i : ι) (x : F i), C ⟦⟨i, x⟩⟧) → ∀ (x : DirectLimit F f), C x
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.lift_comp_ι : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A),
  ↑(SymmetricAlgebra.lift f) ∘ₗ SymmetricAlgebra.ι R M = f
-- Mathlib.CategoryTheory.Filtered.Final
/-- If `C` is filtered, then the structured arrow category on the diagonal functor `C ⥤ C × C`
is filtered as well.  -/
CategoryTheory.instIsFilteredStructuredArrowProdDiagOfIsFilteredOrEmpty : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFilteredOrEmpty C] (X : C × C),
  CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag C))
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
InnerProductSpace.volume_ball_of_dim_odd : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {k : ℕ},
  Module.finrank ℝ E = 2 * k + 1 →
    ∀ (x : E) (r : ℝ),
      MeasureTheory.volume (Metric.ball x r) =
        ENNReal.ofReal r ^ Module.finrank ℝ E *
          ENNReal.ofReal (Real.pi ^ k * 2 ^ (k + 1) / ↑(Module.finrank ℝ E).doubleFactorial)
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
Finsupp.toFreeAbelianGroup_toFinsupp : ∀ {X : Type u_2} (x : FreeAbelianGroup X), Finsupp.toFreeAbelianGroup (FreeAbelianGroup.toFinsupp x) = x
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In a preadditive category, any binary bicone which is a colimit cocone is in fact a
bilimit bicone.  -/
CategoryTheory.Limits.isBinaryBilimitOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        (t : CategoryTheory.Limits.BinaryBicone X Y) → CategoryTheory.Limits.IsColimit t.toCocone → t.IsBilimit
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
WeierstrassCurve.Affine.Point.sym2x_neg_left : ∀ {R : Type u_1} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (P Q : W'.Point), (-P).sym2x Q = P.sym2x Q
-- Mathlib.GroupTheory.Congruence.Defs
Con.comap_id : ∀ {M : Type u_1} [inst : Mul M] (c : Con M), Con.comap id ⋯ c = c
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.inter.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m₁ m₁_1 : Std.ExtHashSet α), m₁ = m₁_1 → ∀ (m₂ m₂_1 : Std.ExtHashSet α), m₂ = m₂_1 → m₁.inter m₂ = m₁_1.inter m₂_1
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein_injective : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r], Function.Injective ⇑(Ordinal.typein r).toRelEmbedding
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instSub : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_4} →
          [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → {n : ℕ∞} → Sub (TestFunction Ω F n)
-- Mathlib.Probability.Martingale.Convergence
/-- An L¹-bounded submartingale has bounded upcrossings almost everywhere.  -/
MeasureTheory.Submartingale.upcrossings_ae_lt_top' : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {a b : ℝ}
  {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    (∀ (n : ℕ), MeasureTheory.eLpNorm (f n) 1 μ ≤ ↑R) → a < b → ∀ᵐ (ω : Ω) ∂μ, MeasureTheory.upcrossings a b f ω < ⊤