mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toListRev.match_1.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.Step → Sort u_3) (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Mathlib.LinearAlgebra.Dimension.Localization
/-- Given `IsScalarTower R S N`, if `S` is the fraction ring of `R`, then the rank `rank S N`
of the right part of the tower equals the rank `rank R N` of the whole tower.

See `IsFractionRing.finrank_right_eq` for the finrank version.  -/
IsFractionRing.rank_right_eq : ∀ (R : Type uR) (S : Type uS) (N : Type uN) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : AddCommGroup N]
  [inst_3 : Module R N] [inst_4 : Algebra R S] [inst_5 : Module S N] [IsScalarTower R S N] [IsFractionRing R S],
  Module.rank S N = Module.rank R N
-- Lean.Meta.Tactic.Grind.Types
/-- The action could not make further progress.
`gs` are subgoals that could not be closed. They are used for producing error messages.
 -/
Lean.Meta.Grind.ActionResult.stuck : List Lean.Meta.Grind.Goal → Lean.Meta.Grind.ActionResult
-- Init.Data.Option.Lemmas
Option.isNone_or : ∀ {α : Type u_1} {o o' : Option α}, (o.or o').isNone = (o.isNone && o'.isNone)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instRightCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : RightCancelMonoid α],
  Colex.instRightCancelMonoid = { toMonoid := Colex.instMonoid, toIsRightCancelMul := ⋯ }
-- Lean.Meta.Constructions.NoConfusion
/-- Creates per-constructor no-confusion definitions. These specialize the general noConfusion
declaration to (homogeneous!) equalities between two applications of the same constructor, to
effectively cache the computation of `noConfusionType` for that constructor:

```
def L.cons.noConfusion.{u_1, u} : {α : Type u} → {P : Sort u_1} →
  {x : α} → {xs : L α} → {x' : α} → {xs' : L α} →
  L.cons x xs = L.cons x' xs' →
  (x = x' → xs = xs' → P) →
  P

def Vec.cons.noConfusion.{u_1, u} : {α : Type u} → {P : Sort u_1} →
  {n : Nat} → {x : α} → {xs : Vec α n} →
  {n' : Nat} → {x' : α} → {xs' : Vec α n'} →
  n + 1 = n' + 1 → Vec.cons x xs ≍ Vec.cons x' xs' →
  (n = n' → x = x' → xs ≍ xs' → P)
  → P
```

These are specialized to equal parameters. The main use of these theorems is `injection` through
`Meta.mkNoConfusion`, which deals with homogeneous equalities, so no need for the generality.

These still accept a heterogeneous equality between the two constructor applications: if we tried
to phrase this theroem with a homogeneous equality, this would force those constructor fields that
appear in indices to be equal, which is too strong: we can have homogenenous equalities between
two constructor applications with different fields but same indices.
 -/
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.mkNoConfusionCtors : Lean.Name → Lean.MetaM Unit
-- Mathlib.Order.Heyting.Basic
codisjoint_hnot_right : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a : α}, Codisjoint a (￢a)
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.lim_of_notMem_U : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P), ∀ x ∉ c.U, c.lim x = 1
-- Mathlib.Combinatorics.SimpleGraph.Density
/-- Finset of edges of a relation between two finsets of vertices.  -/
Rel.interedges : {α : Type u_4} →
  {β : Type u_5} → (r : α → β → Prop) → [(a : α) → DecidablePred (r a)] → Finset α → Finset β → Finset (α × β)
-- Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
/-- Given an `n`-th primitive root of unity `ζ,` we have that `ζ - 1` and `ζ ^ j - 1` are associated
for all `j` coprime with `n`.
`pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum` gives an explicit formula for the unit.  -/
IsPrimitiveRoot.associated_sub_one_pow_sub_one_of_coprime : ∀ {n j : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [IsDomain A],
  IsPrimitiveRoot ζ n → j.Coprime n → Associated (ζ - 1) (ζ ^ j - 1)
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
/-- Multiplication of additive submonoids of a semiring R. The additive submonoid `S * T` is the
smallest R-submodule of `R` containing the elements `s * t` for `s ∈ S` and `t ∈ T`.  -/
AddSubmonoid.mul : {R : Type u_2} → [inst : NonUnitalNonAssocSemiring R] → Mul (AddSubmonoid R)
-- Mathlib.Data.ZMod.Basic
ZMod.castHom_comp : ∀ {n m d : ℕ} (hm : n ∣ m) (hd : m ∣ d),
  (ZMod.castHom hm (ZMod n)).comp (ZMod.castHom hd (ZMod m)) = ZMod.castHom ⋯ (ZMod n)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α},
  k ∈ Std.ExtDHashMap.filterMap f m ↔ ∃ (h : k ∈ m), (f (m.getKey k h) (Std.ExtDHashMap.Const.get m k h)).isSome = true
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyEntourage_nonneg : ∀ {X : Type u_1} {F : Set X} (T : X → X), F.Nonempty → ∀ (U : SetRel X X), 0 ≤ Dynamics.coverEntropyEntourage T F U
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjOpcyclesSelfIso_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {A B : C} (f : A ⟶ B) {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ((HomologicalComplex.single C c j).map f) j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjOpcyclesSelfIso c j B).inv h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjOpcyclesSelfIso c j A).inv
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.adjunction_homEquiv_symm_apply : ∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCatᵒᵖ} (f : X ⟶ AlgebraicGeometry.Scheme.Spec.obj R),
  (AlgebraicGeometry.ΓSpec.adjunction.homEquiv X R).symm f =
    (AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X.toLocallyRingedSpace R).symm
      (AlgebraicGeometry.Scheme.Hom.toLRSHom f)
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesColimitπ₁ : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
  [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)]
  [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)]
  [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)],
  CategoryTheory.Limits.PreservesColimit F CategoryTheory.ShortComplex.π₁
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_eq_get_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅},
  t.min he = t.min?.get ⋯
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.throwBacktrack : {α : Type} → Lean.PrettyPrinter.ParenthesizerM α
-- Mathlib.Analysis.RCLike.Basic
/-- Conjugate as a continuous linear equivalence  -/
RCLike.conjCLE : {K : Type u_1} → [inst : RCLike K] → K ≃L[ℝ] K
-- Mathlib.Algebra.Group.ULift
ULift.addCommMonoid : {α : Type u} → [AddCommMonoid α] → AddCommMonoid (ULift.{u_1, u} α)
-- Std.Http.Protocol.H1.Message
Std.Http.Protocol.H1.instBEqDirection.beq : Std.Http.Protocol.H1.Direction → Std.Http.Protocol.H1.Direction → Bool
-- Mathlib.RingTheory.TensorProduct.Basic
TensorProduct.flip_mk_surjective : ∀ {R : Type u_1} (S : Type u_3) {T : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : Ring T] [inst_4 : Algebra R T],
  Function.Surjective ⇑(algebraMap R T) → Function.Surjective ⇑((TensorProduct.mk R S T).flip 1)
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Functor.coconeTypesEquiv_apply_pt : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) (c : F.CoconeTypes),
  (F.coconeTypesEquiv c).pt = c.pt
-- Mathlib.Data.Set.Basic
Set.ofPred_bijective : ∀ {α : Type u}, Function.Bijective Set.ofPred
-- Init.Data.Order.FactoriesExtra
/-- Creates a `BEq α` instance from an `Ord α` instance.  -/
BEq.ofOrd : (α : Type u) → [Ord α] → BEq α
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1.eq_1 : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  (hm : m ≤ m0) (μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] (f : α → F'),
  MeasureTheory.condExpL1 hm μ f = MeasureTheory.setToFun μ (MeasureTheory.condExpInd F' hm μ) ⋯ f
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.InfiniteNeg.not_infinitePos : ∀ {x : ℝ*}, x.InfiniteNeg → ¬x.InfinitePos
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.InducedCategory.groupoid : {C : Type u} →
  (D : Type u₂) →
    [CategoryTheory.Groupoid D] → (F : C → D) → CategoryTheory.Groupoid (CategoryTheory.InducedCategory D F)
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.homMk_id : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] (v : V),
  CategoryTheory.Cat.FreeRefl.homMk (CategoryTheory.ReflQuiver.id v) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Cat.FreeRefl.mk v)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} {x y : F} (h : W.Nonsingular x y),
  ↑(WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h) =
    ↑(WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (Polynomial.C y))
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- To show a property hold on all `TrivSqZeroExt R M` it suffices to show it holds
on terms of the form `inl r + inr m`.  -/
TrivSqZeroExt.ind : ∀ {R : Type u_3} {M : Type u_4} [inst : AddZeroClass R] [inst_1 : AddZeroClass M] {P : TrivSqZeroExt R M → Prop},
  (∀ (r : R) (m : M), P (TrivSqZeroExt.inl r + TrivSqZeroExt.inr m)) → ∀ (x : TrivSqZeroExt R M), P x
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_ofFin : ∀ (n : Fin UInt8.size), (UInt8.ofFin n).toBitVec = { toFin := n }
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.instHasAnchorExprWithAnchor : Lean.Meta.Grind.HasAnchor Lean.Meta.Grind.ExprWithAnchor
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the second of three points is weakly between the other two, and not equal to the third,
the angle at the third point (reversed) is zero.  -/
Wbtw.angle₁₃₂_eq_zero_of_ne : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, Wbtw ℝ p₁ p₂ p₃ → p₂ ≠ p₃ → EuclideanGeometry.angle p₁ p₃ p₂ = 0
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- On a countable space, two measures are equal if they agree on measurable atoms.  -/
MeasureTheory.ext_of_measurableAtoms : ∀ {α : Type u_1} {m : MeasurableSpace α} [Countable α] {μ ν : MeasureTheory.Measure α},
  (∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)) → μ = ν
-- Mathlib.Algebra.Module.Submodule.Map
LinearMap.comap_domRestrict : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₂₁ : R₂ →+* R}
  (p : Submodule R₂ M₂) (f : M₂ →ₛₗ[σ₂₁] M) (p' : Submodule R M),
  Submodule.comap (f.domRestrict p) p' = Submodule.comap p.subtype (Submodule.comap f p')
-- Lean.Meta.CongrTheorems
/-- Ensures all dependencies for `.eq` are `.fixed`.
 -/
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.fixKindsForDependencies : Lean.Meta.FunInfo → Array Lean.Meta.CongrArgKind → Array Lean.Meta.CongrArgKind
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instHashableBVUnOp.hash : Std.Tactic.BVDecide.BVUnOp → UInt64
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.coe_coe : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : AddZero M] [inst_1 : AddZero N] [inst_2 : FunLike F M N]
  [inst_3 : AddMonoidHomClass F M N] (f : F), ⇑↑f = ⇑f
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instSubHom : {k : Type u} → {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → {A B : Rep.{w, u, v} k G} → Sub (A ⟶ B)
-- Lean.Parser.Extra
Lean.Parser.suppressInsideQuot.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Init.Omega.Coeffs
/-- Shim for `IntList.bmod`.  -/
Lean.Omega.Coeffs.bmod : Lean.Omega.Coeffs → ℕ → Lean.Omega.Coeffs
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.lift_unique : ∀ {α : Type u} {β : Type v} [inst : Group β] {f : α → β} (g : FreeGroup α →* β),
  (∀ (x : α), g (FreeGroup.of x) = f x) → ∀ {x : FreeGroup α}, g x = (FreeGroup.lift f) x
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.lift_σ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X : C},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) 0)
      CategoryTheory.NonPreadditiveAbelian.σ =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
cfc_comp_re : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [inst_4 : StarModule ℂ A] [inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMap.UniqueHom ℂ A]
  [T2Space A] (f : ℝ → ℝ) (a : A),
  autoParam (ContinuousOn f (spectrum ℝ ↑(realPart a))) cfc_comp_re._auto_1 →
    autoParam (IsStarNormal a) cfc_comp_re._auto_3 → cfc (fun x => ↑(f x.re)) a = cfc f ↑(realPart a)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- List of functions used to construct monomials in multiseries.  -/
Tactic.ComputeAsymptotics.Basis : Type
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.isoMk_hom_h₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S}
  (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j))
  (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k))
  (w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreOneHypercover.isoMk._auto_1)
  (w₁₁ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (h₀ i).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_3)
  (w₁₂ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (h₀ j).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_5)
  {i j : E.I₀} (k : E.I₁ i j), (CategoryTheory.PreOneHypercover.isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).hom.h₁ k = (h₁ k).hom
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.support_sup : ∀ {X : AlgebraicGeometry.Scheme} (I J : X.IdealSheafData), (I ⊔ J).support = I.support ⊓ J.support
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.associator_monoidal_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C) {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X₃ Y₃)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) X₃
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂) Y₃)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X₃ Y₃))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁)
              (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂)
              (CategoryTheory.MonoidalCategoryStruct.tensorObj X₃ Y₃)).hom
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
        (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ X₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₃) Y₁
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Y₃))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁)
            (CategoryTheory.MonoidalCategory.tensorμ X₂ X₃ Y₂ Y₃))
          h))
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.pow_bit0 : ∀ {R : Type u_1} [inst : CommSemiring R] {a b c : R} {k : ℕ}, a ^ k = b → b * b = c → a ^ Nat.mul 2 k = c
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.toPerfPair_conj_reflection : ∀ {ι : 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) (i : ι),
  P.toPerfPair.conj ↑(P.reflection i) = (↑(P.coreflection i)).dualMap
-- Mathlib.Topology.Instances.Nat
Nat.closedBall_eq_Icc : ∀ (x : ℕ) (r : ℝ), Metric.closedBall x r = Set.Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
-- Mathlib.Data.List.Perm.Basic
List.forall₂_comp_perm_eq_perm_comp_forall₂ : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop},
  Relation.Comp (List.Forall₂ r) List.Perm = Relation.Comp List.Perm (List.Forall₂ r)
-- Mathlib.Data.Rat.Lemmas
Rat.pnatDen_one : Rat.pnatDen 1 = 1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.cin_cast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α}
  (s : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig1) (hcast : aig1.decls.size ≤ aig2.decls.size),
  (s.cast hcast).cin = s.cin.cast hcast
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instIsLeftCancelMul : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Mul M] [IsLeftCancelMul M], IsLeftCancelMul (l.Germ M)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.ιObj.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.SmallObject.ιObj I κ f =
    CategoryTheory.Arrow.Hom.left ((CategoryTheory.SmallObject.ιIteration I κ).app (CategoryTheory.Arrow.mk f))
-- Mathlib.MeasureTheory.OuterMeasure.Defs
/-- Outer measure function. Use automatic coercion instead.  -/
MeasureTheory.OuterMeasure.measureOf : {α : Type u_2} → MeasureTheory.OuterMeasure α → Set α → ENNReal
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.instMonoIntιObjFactorisationCofFib : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L)
  (F : (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cofFib✝ f).FullSubcategory), CategoryTheory.Mono F.obj.ι
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.measurable_trajFun : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ),
  Measurable (ProbabilityTheory.Kernel.trajFun κ a)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.le_coproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  W ≤ CategoryTheory.MorphismProperty.coproducts.{w, v, u} W
-- Init.Data.UInt.Bitwise
USize.ofBitVec_or : ∀ (a b : BitVec System.Platform.numBits), { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.mem_closure_iff_symm_ball : ∀ {α : Type ua} [inst : UniformSpace α] {s : Set α} {x : α},
  x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ uniformity α → SetRel.IsSymm V → (s ∩ UniformSpace.ball x V).Nonempty
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k a : α} [inst_1 : Inhabited (β a)] {v : β k},
      (Std.DTreeMap.Internal.Impl.insert! k v t).get! a = if h : compare k a = Ordering.eq then cast ⋯ v else t.get! a
-- Mathlib.Order.Interval.Finset.Nat
Nat.cauchy_induction_two_mul : ∀ {P : ℕ → Prop},
  (∀ (n : ℕ), P (n + 1) → P n) → ∀ (seed : ℕ), P seed.succ → (∀ (x : ℕ), seed < x → P x → P (2 * x)) → ∀ (n : ℕ), P n
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  ∅.minKey! = default
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.toClass_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] (P : W.Point),
  WeierstrassCurve.Affine.Point.toClass P = 0 ↔ P = 0
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.dvd_content_iff_C_dvd : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p : Polynomial R} {r : R},
  r ∣ p.content ↔ Polynomial.C r ∣ p
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getEntryLT!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryLT! k = t₂.getEntryLT! k
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.map_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort uι} {f : α → β} {m : ι → MeasurableSpace α},
  MeasurableSpace.map f (⨅ i, m i) = ⨅ i, MeasurableSpace.map f (m i)
-- Mathlib.Topology.Algebra.Group.Torsor
IsTopologicalTorsor.mk : ∀ {V : Type u_1} [inst : Group V] [inst_1 : TopologicalSpace V] {P : Type u_2} [inst_2 : Torsor V P]
  [inst_3 : TopologicalSpace P] [toContinuousSMul : ContinuousSMul V P],
  (Continuous fun x => x.1 /ₛ x.2) → IsTopologicalTorsor P
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_neg_of_mem_ball : ∀ (𝕂 : Type u_1) {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedDivisionRing 𝔸]
  [inst_2 : NormedAlgebra 𝕂 𝔸] [CharZero 𝕂] [CompleteSpace 𝔸] {x : 𝔸},
  x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius → NormedSpace.exp (-x) = (NormedSpace.exp x)⁻¹
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mul_eq_tensor : ∀ {R : Type u} [inst : CommSemiring R] (M N : CommRing.Pic R),
  M * N = CommRing.Pic.mk R (TensorProduct R M.AsModule N.AsModule)