mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObj.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {R : C} →
          [toAddGrpObj : CategoryTheory.AddGrpObj R] →
            [toIsCommAddMonObj : CategoryTheory.IsCommAddMonObj R] →
              [toMonObj : CategoryTheory.MonObj R] →
                CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R CategoryTheory.AddMonObj.add)
                      CategoryTheory.MonObj.mul =
                    CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.CartesianMonoidalCategory.lift
                        (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R
                            (CategoryTheory.SemiCartesianMonoidalCategory.fst R R))
                          CategoryTheory.MonObj.mul)
                        (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R
                            (CategoryTheory.SemiCartesianMonoidalCategory.snd R R))
                          CategoryTheory.MonObj.mul))
                      CategoryTheory.AddMonObj.add →
                  CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add R)
                        CategoryTheory.MonObj.mul =
                      CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.CartesianMonoidalCategory.lift
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                              (CategoryTheory.SemiCartesianMonoidalCategory.fst R R) R)
                            CategoryTheory.MonObj.mul)
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                              (CategoryTheory.SemiCartesianMonoidalCategory.snd R R) R)
                            CategoryTheory.MonObj.mul))
                        CategoryTheory.AddMonObj.add →
                    CategoryTheory.RingObj R
-- Mathlib.Algebra.Group.Support
Function.support_add : ∀ {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (f g : α → M),
  (Function.support fun x => f x + g x) ⊆ Function.support f ∪ Function.support g
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_inv_assoc : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] [inst_6 : F.OplaxRightLinear C] (d : D) (c c' : C)
  {Z : D'}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxRightLinear.δᵣ F
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c')
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
          (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c) c')
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').inv h)) =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorObj c c')) h)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_homothetyUnitsMulHom_eq_homothetyHom_coe : ∀ {R : Type u_10} {V : Type u_11} {P : Type u_12} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : AddTorsor V P] (p : P),
  AffineEquiv.toAffineMap ∘ ⇑(AffineEquiv.homothetyUnitsMulHom p) = ⇑(AffineMap.homothetyHom p) ∘ Units.val
-- Mathlib.CategoryTheory.Limits.Opposites
/-- The colimit of `F.unop` is the unopposite of `limit F`.  -/
CategoryTheory.Limits.colimitUnopIsoOpLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            CategoryTheory.Limits.colimit F.unop ≅ Opposite.unop (CategoryTheory.Limits.limit F)
-- Mathlib.Order.Completion
DedekindCut.principalEmbedding_apply : ∀ {α : Type u_1} [inst : PartialOrder α] (a : α), DedekindCut.principalEmbedding a = DedekindCut.principal a
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContextEntry.localVar.injEq : ∀ (a : Lean.IR.IRType) (a_1 : Lean.IR.Expr) (a_2 : Lean.IR.IRType) (a_3 : Lean.IR.Expr),
  (Lean.IR.LocalContextEntry.localVar a a_1 = Lean.IR.LocalContextEntry.localVar a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.instCanLiftSetCoeAndForallForallForallMemForallHAddForallForallForallForallHMulForallCoeRingHomAlgebraMap : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  CanLift (Set A) (Subalgebra R A) SetLike.coe fun s =>
    (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
      (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R), (algebraMap R A) r ∈ s
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.linearYoneda_obj_map : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] (X : C) {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
  ((CategoryTheory.linearYoneda R C).obj X).map f = ModuleCat.ofHom (CategoryTheory.Linear.leftComp R X f.unop)
-- Mathlib.Data.Finset.Image
Finset.map_subset_map : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s₁ s₂ : Finset α}, Finset.map f s₁ ⊆ Finset.map f s₂ ↔ s₁ ⊆ s₂
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.components.eq_1 : ∀ {J : Type} [inst : Finite J] {K : Type} [inst_1 : Finite K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C}
  {g : K → C} (m : ⨁ f ⟶ ⨁ g) (j : J) (k : K),
  CategoryTheory.Limits.biproduct.components m j k =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
      (CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.biproduct.π g k))
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Methods.post : Lean.Meta.Sym.Simp.Methods → Lean.Meta.Sym.Simp.Simproc
-- Init.Data.Slice.List.Lemmas
ListSlice.mkSlice_roi_eq_mkSlice_rci : ∀ {α : Type u_1} {xs : ListSlice α} {lo : ℕ},
  Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Rci.Sliceable.mkSlice xs (lo + 1)...*
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.curryAlgEquiv.eq_1 : ∀ (R : Type u_1) {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N],
  MonoidAlgebra.curryAlgEquiv R =
    { toEquiv := MonoidAlgebra.curryRingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Init.Data.Vector.Lemmas
Vector.getElem?_cast : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {w : n = m} {i : ℕ}, (Vector.cast w xs)[i]? = xs[i]?
-- Mathlib.Data.Finset.Empty
Finset.not_nonempty_empty : ∀ {α : Type u_1}, ¬∅.Nonempty
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_insert : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : (↑m).WF) {k a : α} {v : β}
  {h₁ : (m.insert k v).contains a = true},
  Std.DHashMap.Internal.Raw₀.Const.get (m.insert k v) a h₁ =
    if h₂ : (k == a) = true then v else Std.DHashMap.Internal.Raw₀.Const.get m a ⋯
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.contains_filterMap_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α},
  (↑m).WF →
    ((Std.DHashMap.Internal.Raw₀.filterMap f m).contains k = true ↔
      ∃ (h' : m.contains k = true), (f (m.getKey k h') (Std.DHashMap.Internal.Raw₀.Const.get m k h')).isSome = true)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  [inst_2 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.TreeMap.Raw.ofList l cmp).getKey! k = default
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.rTensor_exact_iff_exact : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N1 : Type u_1}
  [inst_3 : AddCommGroup N1] [inst_4 : Module R N1] {N2 : Type u_2} [inst_5 : AddCommGroup N2] [inst_6 : Module R N2]
  {N3 : Type u_3} [inst_7 : AddCommGroup N3] [inst_8 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3)
  [Module.FaithfullyFlat R M],
  Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23) ↔ Function.Exact ⇑l12 ⇑l23
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.reduce_isReduced : ∀ (u : PNat.XgcdType), u.reduce.IsReduced
-- Mathlib.Data.Nat.Factorial.Basic
/-- **Alias** of the reverse direction of `Nat.descFactorial_eq_zero_iff_lt`. -/
Nat.descFactorial_of_lt : ∀ {n k : ℕ}, n < k → n.descFactorial k = 0
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.natDegree_reflect_le : ∀ {R : Type u_1} [inst : Semiring R] {N : ℕ} {p : Polynomial R}, (Polynomial.reflect N p).natDegree ≤ max N p.natDegree
-- Mathlib.Condensed.Discrete.Colimit
CategoryTheory.Functor.leftKanExtensionUniqueOfIso.congr_simp : ∀ {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}
  (α α_1 : F ⟶ L.comp F') (e_α : α = α_1) [inst_3 : F'.IsLeftKanExtension α] {G : CategoryTheory.Functor C H}
  (i i_1 : F ≅ G),
  i = i_1 →
    ∀ (G' : CategoryTheory.Functor D H) (β β_1 : G ⟶ L.comp G') (e_β : β = β_1) [inst_4 : G'.IsLeftKanExtension β],
      F'.leftKanExtensionUniqueOfIso α i G' β = F'.leftKanExtensionUniqueOfIso α_1 i_1 G' β_1
-- Mathlib.Combinatorics.Colex
Finset.Colex.initSeg_nonempty : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} [inst_1 : Fintype α], (Finset.Colex.initSeg s).Nonempty
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Iic₀ : ∀ {G₀ : Type u_2} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {c : G₀} (a : G₀),
  0 < c → (fun x => c * x) ⁻¹' Set.Iic a = Set.Iic (a / c)
-- Mathlib.Order.TypeTags
WithTop.instRepr : {α : Type u_1} → [Repr α] → Repr (WithTop α)
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instInhabitedOffset : Inhabited Std.Time.Millisecond.Offset
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
IsBaseChange.basis.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {V : Type u_3}
  [inst_3 : AddCommMonoid V] [inst_4 : Module R V] {W : Type u_4} [inst_5 : AddCommMonoid W] [inst_6 : Module R W]
  [inst_7 : Module S W] [inst_8 : IsScalarTower R S W] {ι : Type u_5} {ε ε_1 : V →ₗ[R] W} (e_ε : ε = ε_1)
  (b b_1 : Module.Basis ι R V),
  b = b_1 → ∀ (ibc : IsBaseChange S ε), IsBaseChange.basis b ibc = IsBaseChange.basis b_1 ⋯
-- Init.Data.Option.Lemmas
Option.isNone_merge : ∀ {α : Type u_1} {o o' : Option α} {f : α → α → α}, (Option.merge f o o').isNone = (o.isNone && o'.isNone)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.mk_ker : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided], RingHom.ker (Ideal.Quotient.mk I) = I
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.extendLeft_length : ∀ {n : ℕ} (c : OrderedFinpartition n), c.extendLeft.length = c.length + 1
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Coframe.toSDiff : {α : Type u_1} → [self : Order.Coframe α] → SDiff α
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyLike.toContinuousMapClass : ∀ {X : outParam (Type u_3)} {Y : outParam (Type u_4)} {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y}
  {F : Type u_5} {f₀ f₁ : outParam C(X, Y)} {inst_2 : FunLike F (↑unitInterval × X) Y}
  [self : ContinuousMap.HomotopyLike F f₀ f₁], ContinuousMapClass F (↑unitInterval × X) Y
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.forInUncurried_eq_forIn_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {δ : Type w} {m' : Type w → Type w'} {β : Type v}
  {m : Std.DHashMap α fun x => β} [inst : Monad m'] [LawfulMonad m'] {f : α × β → δ → m' (ForInStep δ)} {init : δ},
  Std.DHashMap.Const.forInUncurried f init m = forIn (Std.DHashMap.Const.toList m) init f
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Icc_uIcc_uIcc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α},
  Filter.TendstoIxxClass Set.Icc (Filter.principal (Set.uIcc a b)) (Filter.principal (Set.uIcc a b))
-- Mathlib.Analysis.Convex.Basic
convex_segment : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [IsOrderedRing 𝕜] (x y : E), Convex 𝕜 (segment 𝕜 x y)
-- Mathlib.Logic.Nontrivial.Basic
Subtype.nontrivial_iff_exists_ne : ∀ {α : Type u_1} (p : α → Prop) (x : Subtype p), Nontrivial (Subtype p) ↔ ∃ y, ∃ (_ : p y), y ≠ ↑x
-- Init.Data.Vector.Lemmas
Vector.map_flatten : ∀ {α : Type u_1} {β : Type u_2} {n m : ℕ} {f : α → β} {xss : Vector (Vector α n) m},
  Vector.map f xss.flatten = (Vector.map (Vector.map f) xss).flatten
-- Mathlib.Topology.LocallyFinite
LocallyFinite.preimage_continuous : ∀ {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : ι → Set X}
  {g : Y → X}, LocallyFinite f → Continuous g → LocallyFinite fun x => g ⁻¹' f x
-- Mathlib.MeasureTheory.Integral.TorusIntegral
/-- If `f` and `g` are two torus integrable functions, then so is `f + g`.  -/
TorusIntegrable.add : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] {f g : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ},
  TorusIntegrable f c R → TorusIntegrable g c R → TorusIntegrable (f + g) c R
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) {Y : TopCat}
  {f : Y ⟶ TopCat.of ↑↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (U : TopologicalSpace.Opens ↑↑(X.restrict h)),
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U =
    CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U))
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.closure_add_le : ∀ {M : Type u_3} [inst : AddMonoid M] (S T : Set M),
  AddSubmonoid.closure (S + T) ≤ AddSubmonoid.closure S ⊔ AddSubmonoid.closure T
-- Mathlib.Algebra.Lie.Weights.Killing
LieModule.Weight.isZero_neg : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] [inst_4 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_5 : H.IsCartanSubalgebra] [inst_6 : LieModule.IsTriangularizable K (↥H) L] {α : LieModule.Weight K (↥H) L},
  (-α).IsZero ↔ α.IsZero
-- Mathlib.Algebra.Free
FreeMagma.toFreeSemigroup_comp_map : ∀ {α : Type u} {β : Type v} (f : α → β),
  FreeMagma.toFreeSemigroup.comp (FreeMagma.map f) = (FreeSemigroup.map f).comp FreeMagma.toFreeSemigroup
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- If `I` is a nonzero fractional ideal, `a ∈ R`, and `J` is an ideal of `R` such that
`I = a⁻¹J`, then `I` is equal to the product `∏_v v^(val_v(J) - val_v(a))`.  -/
FractionalIdeal.finprod_heightOneSpectrum_factorization : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {I : FractionalIdeal (nonZeroDivisors R) K},
  I ≠ 0 →
    ∀ {a : R} {J : Ideal R},
      I = FractionalIdeal.spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * ↑J →
        ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R),
            ↑v.asIdeal ^
              (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
                ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) =
          I
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.pairwiseDisjoint_smul_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β] {s : Set α}
  {t : Finset β}, (∀ a ∈ s, a ≠ 0) → ((s.PairwiseDisjoint fun x => x • t) ↔ Set.InjOn (fun p => p.1 • p.2) (s ×ˢ ↑t))
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.supportAddSubgroup_eq : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R} [inst_1 : P.HasIdealSupport],
  P.supportAddSubgroup = Submodule.toAddSubgroup P.support
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Real.sinc_of_ne_zero : ∀ {x : ℝ}, x ≠ 0 → Real.sinc x = Real.sin x / x
-- Mathlib.Order.WellQuasiOrder
WellQuasiOrdered.wellFounded : ∀ {α : Type u_3} {r : α → α → Prop} [IsPreorder α r], WellQuasiOrdered r → WellFounded fun a b => r a b ∧ ¬r b a
-- Init.Data.SInt.Lemmas
Int32.toInt64_neg_of_ne : ∀ {x : Int32}, x ≠ -2147483648 → (-x).toInt64 = -x.toInt64
-- Init.Data.List.Erase
List.length_eraseIdx_le : ∀ {α : Type u_1} (l : List α) (i : ℕ), (l.eraseIdx i).length ≤ l.length
-- Std.Data.HashSet.Lemmas
Std.HashSet.containsThenInsert_snd : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {k : α}, (m.containsThenInsert k).2 = m.insert k
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instPropAsSPredTautologyDown : ∀ {φ : Std.Do.SPred []}, Std.Do.SPred.Tactic.PropAsSPredTautology φ.down φ
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Ioc_left_eq_Ioc_pred : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  a ≤ b → insert a (Set.Ioc a b) = Set.Ioc (Order.pred a) b
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.size_updateBucket : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α] {self : Array (Std.DHashMap.Internal.AssocList α β)}
  {h : 0 < self.size} {k : α} {f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β},
  (Std.DHashMap.Internal.updateBucket self h k f).size = self.size
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.filter.go.eq_2 : ∀ {α : Type u} {β : α → Type v} (f : (a : α) → β a → Bool) (acc : Std.DHashMap.Internal.AssocList α β) (a : α) (b : β a)
  (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.filter.go✝ f acc (Std.DHashMap.Internal.AssocList.cons a b es) =
    bif f a b then Std.DHashMap.Internal.AssocList.filter.go✝ f (Std.DHashMap.Internal.AssocList.cons a b acc) es
    else Std.DHashMap.Internal.AssocList.filter.go✝ f acc es
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst.eq_3 : ∀ (n : ℕ), n.succ.stirlingFirst 0 = 0
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find?_eq_some_find_of_exists : ∀ {n : ℕ} {p : Fin n → Bool} (h : ∃ i, p i = true), Fin.find? p = some (Fin.find (fun x => p x = true) h)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Algebra.QuasiFiniteAt.eq_1 : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S)
  [inst_3 : p.IsPrime], Algebra.QuasiFiniteAt R p = Algebra.QuasiFinite R (Localization.AtPrime p)
-- Mathlib.Tactic.NormNum.Result
/-- Extract from a `Result` the rational value (as both a term and an expression),
and the proof that the original expression is equal to this rational number.
 -/
Mathlib.Meta.NormNum.Result.toRat' : {u : Lean.Level} →
  {α : Q(Type u)} →
    {e : Q(«$α»)} →
      (_i : autoParam Q(DivisionRing «$α») Mathlib.Meta.NormNum.Result.toRat'._auto_1) →
        Mathlib.Meta.NormNum.Result e →
          Option (ℚ × (n : Q(ℤ)) × (d : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsRat «$e» «$n» «$d»))
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Goal.getTarget? : Lean.Meta.Grind.Goal → Lean.Expr → Option Lean.Expr
-- Mathlib.Algebra.Category.ModuleCat.Algebra
ModuleCat.isScalarTower_of_algebra_moduleCat : ∀ {k : Type u} [inst : Field k] {A : Type w} [inst_1 : Ring A] [inst_2 : Algebra k A] (M : ModuleCat A),
  IsScalarTower k A ↑M
-- Mathlib.Data.Finset.Sups
Finset.infs_self : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s : Finset α}, s ⊼ s = s ↔ InfClosed ↑s
-- Init.Data.List.Nat.Range
List.mem_zipIdx : ∀ {α : Type u_1} {x : α} {i : ℕ} {xs : List α} {k : ℕ} (h : (x, i) ∈ xs.zipIdx k),
  k ≤ i ∧ i < k + xs.length ∧ x = xs[i - k]
-- Mathlib.Algebra.Group.UniqueProds.Basic
TwoUniqueProds.toUniqueProds : ∀ (G : Type u_1) [inst : Mul G] [TwoUniqueProds G], UniqueProds G
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Homotopy.extend_ofExtend : ∀ {ι : 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.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {K L : HomologicalComplex C c} {f g : K ⟶ L} {e : c.Embedding c'}
  [inst_3 : e.IsRelIff] (h : Homotopy (HomologicalComplex.extendMap f e) (HomologicalComplex.extendMap g e)),
  h.ofExtend.extend e = h
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
/-- The isomorphism between the sheafification of `P` composed with `F` and
the sheafification of `P ⋙ F`, functorially in `F`.  -/
CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          {E : Type u_2} →
            [inst_2 : CategoryTheory.Category.{v_2, u_2} E] →
              [inst_3 :
                  ∀ (J : CategoryTheory.Limits.MulticospanShape),
                    CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] →
                [inst_4 :
                    ∀ (J : CategoryTheory.Limits.MulticospanShape),
                      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] →
                  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
                    [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] →
                      (P : CategoryTheory.Functor Cᵒᵖ D) →
                        [∀ (F : CategoryTheory.Functor D E) (X : C),
                              CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] →
                          [∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X)
                                (P : CategoryTheory.Functor Cᵒᵖ D),
                                CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] →
                            (CategoryTheory.Functor.whiskeringLeft Cᵒᵖ D E).obj (J.sheafify P) ≅
                              ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ D E).obj P).comp (J.sheafification E)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.instUniqueHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk : Unique ((SSet.truncation 2).obj (SSet.stdSimplex.obj { len := 0 })).HomotopyCategory