mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π : ∀ {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]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_5 : CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)]
  {j : J} {k : K},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim G).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π
          ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).comp CategoryTheory.Limits.lim) k)
        (CategoryTheory.Limits.limit.π
          ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).obj k) j)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) j)
      (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).obj j) k)
-- Mathlib.Analysis.Normed.Lp.lpSpace
one_memℓp_infty : ∀ {I : Type u_5} {B : I → Type u_6} [inst : (i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)], Memℓp 1 ⊤
-- Mathlib.Topology.UniformSpace.Equicontinuity
Set.EquicontinuousAt.mono : ∀ {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {H H' : Set (X → α)} {x₀ : X},
  H.EquicontinuousAt x₀ → H' ⊆ H → H'.EquicontinuousAt x₀
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.inverse.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {A : Type u_4} [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A] {B₁ : Type u_6}
  [inst_3 : Monoid B₁] [inst_4 : MulDistribMulAction M B₁] (f : A →*[M] B₁) (g : B₁ → A)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f),
  f.inverse g h₁ h₂ = { toFun := g, map_smul' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.IsUnitTrinomial.trailingCoeff_isUnit : ∀ {p : Polynomial ℤ}, p.IsUnitTrinomial → IsUnit p.trailingCoeff
-- Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject
CategoryTheory.SimplicialObject.instEnrichedCategorySSet : {D : Type u} →
  [inst : CategoryTheory.Category.{v, u} D] → CategoryTheory.EnrichedCategory SSet (CategoryTheory.SimplicialObject D)
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.const_ne_one : ∀ {ι : Type u_1} {α : Type u_2} [inst : One α] [Nonempty ι] {a : α}, Function.const ι a ≠ 1 ↔ a ≠ 1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateDel! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.FVarId → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_uInt64ToNat : ∀ (n : UInt64) (h : n.toNat < UInt32.size), UInt32.ofNatLT n.toNat h = n.toUInt32
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Action : Type
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_diff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β},
  (m₁ \ m₂).getD k fallback = if k ∈ m₂ then fallback else m₁.getD k fallback
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.integrable_comp_mul_left_iff : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] (g : ℝ → F) {R : ℝ},
  R ≠ 0 →
    (MeasureTheory.Integrable (fun x => g (R * x)) MeasureTheory.volume ↔
      MeasureTheory.Integrable g MeasureTheory.volume)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverExtension.modifyState : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → (σ → σ) → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Order.WithBotTop
WithBotTop.rec_top : ∀ {ι : Type u_1} {motive : WithBotTop ι → Sort u_2} (bot : motive ⊥) (coe : (a : ι) → motive (WithBotTop.coe a))
  (top : motive ⊤), WithBotTop.rec bot coe top ⊤ = top
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- The right homology data of `(K.extend e).sc' i' j' k'` that is deduced
from a right homology data of `K.sc' i j k`.  -/
HomologicalComplex.extend.rightHomologyData : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {i j k : ι} →
                      {i' j' k' : ι'} →
                        e.f j = j' →
                          c.prev j = i →
                            c'.prev j' = i' →
                              c.next j = k →
                                c'.next j' = k' →
                                  (K.sc' i j k).RightHomologyData → ((K.extend e).sc' i' j' k').RightHomologyData
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.liftOfIsRightKanExtension_fac : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] (G : CategoryTheory.Functor D H) (β : L.comp G ⟶ F),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft (F'.liftOfIsRightKanExtension α G β)) α = β
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
CategoryTheory.Limits.WalkingMulticospan.instFinCategoryOfLOfDecidableEqR : {J : CategoryTheory.Limits.MulticospanShape} →
  [Fintype J.L] →
    [Fintype J.R] →
      [DecidableEq J.L] → [DecidableEq J.R] → CategoryTheory.FinCategory (CategoryTheory.Limits.WalkingMulticospan J)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_filter : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → Bool},
  (Std.DHashMap.Internal.toListModel (↑(Std.DHashMap.Internal.Raw₀.filter f m)).buckets).Perm
    (List.filter (fun p => f p.fst p.snd) (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.Topology.UniformSpace.Cauchy
CauchySeq.tendsto_uniformity : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : Preorder β] {u : β → α},
  CauchySeq u → Filter.Tendsto (Prod.map u u) Filter.atTop (uniformity α)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_inv_naturality_middle : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Y' : C}
  (f : Y ⟶ Y') (Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z))
      (CategoryTheory.MonoidalCategoryStruct.associator X Y' Z).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) Z)
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?_eq_utf8DecodeChar?_extract : ∀ {b : ByteArray} {i : ℕ}, b.utf8DecodeChar? i = (b.extract i b.size).utf8DecodeChar? 0
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.im_add : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a b : QuaternionAlgebra R c₁ c₂ c₃) [inst : AddZeroClass R], (a + b).im = a.im + b.im
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.id_whiskerLeft_bimod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y : CategoryTheory.Mon C} {M N : Bimod X Y} (f : M ⟶ N),
  (Bimod.regular X).whiskerLeft f =
    CategoryTheory.CategoryStruct.comp M.leftUnitorBimod.hom
      (CategoryTheory.CategoryStruct.comp f N.leftUnitorBimod.inv)
-- Lean.Util.Diff
_private.Lean.Util.Diff.0.Lean.Diff.matchPrefix.go : {α : Type u_1} → [BEq α] → Subarray α → Subarray α → Array α → Array α × Subarray α × Subarray α
-- Mathlib.Algebra.Ring.Action.End
/-- Each element of the group defines a ring automorphism.

This is a stronger version of `DistribMulAction.toAddAut` and
`MulDistribMulAction.toMulAut`.  -/
MulSemiringAction.toRingAut : (G : Type u_1) → (R : Type u_2) → [inst : Group G] → [inst_1 : Semiring R] → [MulSemiringAction G R] → G →* RingAut R
-- Mathlib.Algebra.MvPolynomial.Comap
/-- If two polynomial types over the same coefficient ring `R` are equivalent,
there is a bijection between the types of functions from their variable types to `R`.
 -/
MvPolynomial.comapEquiv : {σ : Type u_1} →
  {τ : Type u_2} →
    {R : Type u_4} → [inst : CommSemiring R] → (MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R) → (τ → R) ≃ (σ → R)
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- If a word reduces to another word, then they have a common maximal reduction.  -/
FreeGroup.reduce.eq_of_red : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.Red L₁ L₂ → FreeGroup.reduce L₁ = FreeGroup.reduce L₂
-- Lean.Declaration
Lean.Declaration.foldExprM : {α : Type} → {m : Type → Type} → [Monad m] → Lean.Declaration → (α → Lean.Expr → m α) → α → m α
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- `CompactlySupportedContinuousMapClass F α β` states that `F` is a type of continuous maps with
compact support.

You should also extend this typeclass when you extend `CompactlySupportedContinuousMap`.  -/
CompactlySupportedContinuousMapClass : (F : Type u_5) →
  (α : outParam (Type u_6)) →
    (β : outParam (Type u_7)) → [TopologicalSpace α] → [Zero β] → [TopologicalSpace β] → [FunLike F α β] → Prop
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.sbtw : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ → s.radius ≠ 0 → Sbtw ℝ p₁ s.center p₂
-- Mathlib.Data.Num.Bitwise
Num.lxor_eq_xor : ∀ (p q : Num), p.lxor q = p ^^^ q
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor.mk.inj : ∀ {toPreprocessorBase : Mathlib.Tactic.Linarith.PreprocessorBase}
  {transform : Lean.MVarId → List Lean.Expr → Lean.MetaM (List Mathlib.Tactic.Linarith.Branch)}
  {toPreprocessorBase_1 : Mathlib.Tactic.Linarith.PreprocessorBase}
  {transform_1 : Lean.MVarId → List Lean.Expr → Lean.MetaM (List Mathlib.Tactic.Linarith.Branch)},
  { toPreprocessorBase := toPreprocessorBase, transform := transform } =
      { toPreprocessorBase := toPreprocessorBase_1, transform := transform_1 } →
    toPreprocessorBase = toPreprocessorBase_1 ∧ transform = transform_1
-- Mathlib.Data.FunLike.IsApply
IsInvApply.inv_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Inv β}
  {inst_2 : Inv F} [self : IsInvApply F α β] (f : F) (x : α), f⁻¹ x = (f x)⁻¹
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Every nonzero element of a group with zero is invertible.  -/
GroupWithZero.mul_inv_cancel : ∀ {G₀ : Type u} [self : GroupWithZero G₀] (a : G₀), a ≠ 0 → a * a⁻¹ = 1
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.checkSyntaxCat : Lean.Linter.MissingDocs.SimpleHandler
-- Mathlib.CategoryTheory.Localization.Prod
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₂ : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {E : Type u₅} [inst_2 : CategoryTheory.Category.{v₅, u₅} E]
  (F : CategoryTheory.Functor (C₁ × C₂) E) (hF : (W₁.prod W₂).IsInvertedBy F) [inst_3 : W₁.ContainsIdentities]
  [inst_4 : W₂.ContainsIdentities],
  W₂.Q.comp
      (CategoryTheory.Functor.curry.obj
          (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift F hF)).flip =
    (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁ F hF).flip
-- Mathlib.Data.Fintype.Sets
FinsetCoe.fintype : {α : Type u_1} → (s : Finset α) → Fintype ↑↑s
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorization_eq_zero_of_not_prime : ∀ (n : ℕ) {p : ℕ}, ¬Nat.Prime p → n.factorization p = 0
-- Mathlib.Algebra.Algebra.Basic
Algebra.instSubtypeMemSubringCenter : {R : Type u_4} → [inst : Ring R] → Algebra (↥(Subring.center R)) R
-- Mathlib.Order.WithBot
WithBot.le_coe_iff : ∀ {α : Type u_1} {b : α} [inst : LE α] {x : WithBot α}, x ≤ ↑b ↔ ∀ (a : α), x = ↑a → a ≤ b
-- Mathlib.RingTheory.Polynomial.GaussNorm
/-- If `v` is a nonnegative nonarchimedean multiplicative function with `v 0 = 0` and `c` is
nonnegative, then the Gauss norm is submultiplicative.  -/
Polynomial.gaussNorm_mul_le : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) {c : ℝ} [ZeroHomClass F R ℝ]
  [NonnegHomClass F R ℝ] [MulHomClass F R ℝ],
  IsNonarchimedean ⇑v →
    ∀ (p q : Polynomial R),
      0 ≤ c → Polynomial.gaussNorm v c (p * q) ≤ Polynomial.gaussNorm v c p * Polynomial.gaussNorm v c q
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.injective : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Nontrivial R], LinearIndependent R v → Function.Injective v
-- Mathlib.Order.Bounds.Basic
lub_Iio_eq_self_or_Iio_eq_Iic : ∀ {γ : Type u_3} [inst : PartialOrder γ] {j : γ} (i : γ), IsLUB (Set.Iio i) j → j = i ∨ Set.Iio i = Set.Iic j
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.isSubDPIdeal_map_of_isSubDPIdeal : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} [inst_1 : CommSemiring B]
  {J : Ideal B} {hJ : DividedPowers J} {f : A →+* B},
  hI.IsDPMorphism hJ f → ∀ {K : Ideal A}, hI.IsSubDPIdeal K → hJ.IsSubDPIdeal (Ideal.map f K)
-- Mathlib.Algebra.CharP.CharAndCard
charP_of_card_eq_prime_pow : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [inst_2 : Fintype R] {p f : ℕ} [hp : Fact (Nat.Prime p)],
  Fintype.card R = p ^ f → CharP R p
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_smul_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} (a : ENNReal) [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ],
  (a • μ).compProd κ = a • μ.compProd κ
-- Lean.Message
Lean.TraceData.mk.inj : ∀ {cls : Lean.Name} {result? : Option Lean.TraceResult} {startTime stopTime : Float} {collapsed : Bool} {tag : String}
  {cls_1 : Lean.Name} {result?_1 : Option Lean.TraceResult} {startTime_1 stopTime_1 : Float} {collapsed_1 : Bool}
  {tag_1 : String},
  { cls := cls, result? := result?, startTime := startTime, stopTime := stopTime, collapsed := collapsed, tag := tag } =
      { cls := cls_1, result? := result?_1, startTime := startTime_1, stopTime := stopTime_1, collapsed := collapsed_1,
        tag := tag_1 } →
    cls = cls_1 ∧
      result? = result?_1 ∧ startTime = startTime_1 ∧ stopTime = stopTime_1 ∧ collapsed = collapsed_1 ∧ tag = tag_1
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.centralizer_le : ∀ {R : Type u_1} [inst : Semiring R] (s t : Set R), s ⊆ t → Subsemiring.centralizer t ≤ Subsemiring.centralizer s
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.ext_iff : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {f g : CuspForm Γ k}, f = g ↔ ∀ (x : UpperHalfPlane), f x = g x
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.any_toArray : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {p : β → Bool}, it.toArray.any p = Std.Iter.any p it
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cocone F} {t : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (w : F ≅ G),
  CategoryTheory.CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).inv (P.desc r) = Q.map r w.inv
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_finsetSum' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε' : Type u_8} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddCommMonoid ε'] [ContinuousAdd ε'] {ι : Type u_9} (s : Finset ι) {f : ι → α → ε'},
  (∀ i ∈ s, MeasureTheory.Integrable (f i) μ) → MeasureTheory.Integrable (∑ i ∈ s, f i) μ
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.symm_bijective : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B], Function.Bijective StarRingEquiv.symm
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.exists_primitive_lcm_of_isPrimitive : ∀ {R : Type u_1} [inst : CommRing R] [NormalizedGCDMonoid R] {p q : Polynomial R},
  p.IsPrimitive → q.IsPrimitive → ∃ r, r.IsPrimitive ∧ ∀ (s : Polynomial R), p ∣ s ∧ q ∣ s ↔ r ∣ s
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instNonUnitalCommRing : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [NonUnitalCommRing β] → NonUnitalCommRing (MeasureTheory.SimpleFunc α β)
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULift.equivalence_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.ULift.equivalence.inverse = CategoryTheory.ULift.downFunctor
-- Mathlib.Order.WithBot
WithTop.lt_def : ∀ {α : Type u_1} [inst : LT α] {x y : WithTop α}, x < y ↔ (∃ a, x = ↑a) ∧ y = ⊤ ∨ ∃ a b, a < b ∧ x = ↑a ∧ y = ↑b
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
/-- The weak kernel built from `weakKernel.ι f` is weakly limiting.  -/
CategoryTheory.Limits.weakKernelIsWeakKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasWeakKernel f] →
            CategoryTheory.Limits.IsWeakLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Limits.weakKernel.ι f) ⋯)
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberMapObjIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (X : C)
  (x : Φ.fiber.obj X),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (F.op.comp P)) (Φ.presheafFiberMapObjIso F K P).inv =
    Φ.toPresheafFiberMap F K P X x
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerSkip_flatMapM_pure : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [inst_3 : Std.Iterator α Id β] [inst_4 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)} {it₁ : Std.Iter β}
  {it₂ it₂' : Std.IterM m γ},
  it₂.IsPlausibleStep (Std.IterStep.skip it₂') →
    (Std.Iter.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep
      (Std.IterStep.skip (Std.Iter.flatMapAfterM f it₁ (some it₂')))
-- Mathlib.Algebra.Algebra.Operations
Submodule.map_op_mul : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M N : Submodule R A),
  Submodule.map (↑(MulOpposite.opLinearEquiv R)) (M * N) =
    Submodule.map (↑(MulOpposite.opLinearEquiv R)) N * Submodule.map (↑(MulOpposite.opLinearEquiv R)) M
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.ι_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y),
  s.ι.app { as := CategoryTheory.Limits.WalkingPair.left } = s.inl
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerRight_actionHomLeft : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' : C} (c'' : C) (f : c ⟶ c') (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c'') d =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c'' d).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c'' d))
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c' c'' d).inv)
-- Batteries.Data.ByteArray
ByteArray.get_extract : ∀ {i : ℕ} {a : ByteArray} {start stop : ℕ} (h : i < (a.extract start stop).size),
  (a.extract start stop)[i] = a[start + i]
-- Mathlib.Analysis.Normed.Module.Basic
NormedField.noncompactSpace : ∀ (𝕜 : Type u_1) [inst : NormedField 𝕜] [Infinite 𝕜], NoncompactSpace 𝕜
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.edist_dist : ∀ {α : Type u} [self : PseudoMetricSpace α] (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- By definition, if `x` is invertible then `inverse x = x⁻¹`.  -/
Ring.inverse_unit : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (u : M₀ˣ), Ring.inverse ↑u = ↑u⁻¹
-- Mathlib.Geometry.Euclidean.Angle.Sphere
_private.Mathlib.Geometry.Euclidean.Angle.Sphere.0.EuclideanGeometry.termO : Lean.ParserDescr
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_inv_mul_iff_mul_le : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a b c : α}, b ≤ a⁻¹ * c ↔ a * b ≤ c
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.FinMeasSupp.map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [inst : Zero β] [inst_1 : Zero γ]
  {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} {g : β → γ},
  f.FinMeasSupp μ → g 0 = 0 → (MeasureTheory.SimpleFunc.map g f).FinMeasSupp μ
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instBot.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  Subgroup.instBot =
    {
      bot :=
        let __src := ⊥;
        { toSubmonoid := __src, inv_mem' := ⋯ } }
-- Mathlib.Topology.DiscreteSubset
/-- The union of finitely many discrete closed subsets is discrete.  -/
discreteTopology_biUnion_finset : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_3} {I : Finset ι} {s : ι → Set X},
  (∀ i ∈ I, DiscreteTopology ↑(s i)) → (∀ i ∈ I, IsClosed (s i)) → DiscreteTopology ↑(⋃ i ∈ I, s i)
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
finiteDimensional_bot : ∀ (K : Type u) (V : Type v) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  FiniteDimensional K ↥⊥
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.inclusion_apply : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {K K' : LieSubalgebra R L} (h : K ≤ K') (x : ↥K), (LieSubalgebra.inclusion h) x = ⟨↑x, ⋯⟩