mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Maps.Proper.CompactlyGenerated
/-- If `Y` is Hausdorff and compactly generated, then proper maps `X → Y` are exactly
continuous maps such that the preimage of any compact set is compact. This is in particular true
if `Y` is Hausdorff and sequential or locally compact.

There was an older version of this theorem which was changed to this one to make use
of the `CompactlyGeneratedSpace` typeclass. (since 2024-11-10)  -/
isProperMap_iff_isCompact_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y]
  [CompactlyCoherentSpace Y] {f : X → Y},
  IsProperMap f ↔ Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
-- Mathlib.Algebra.Group.Invertible.Defs
mul_invOf_cancel_right : ∀ {α : Type u} [inst : Monoid α] (a b : α) [inst_1 : Invertible b], a * b * ⅟b = a
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.coe_mrangeRestrict : ∀ {M : Type u_1} [inst : MulOneClass M] {N : Type u_5} [inst_1 : MulOneClass N] (f : M →* N) (x : M),
  ↑(f.mrangeRestrict x) = f x
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.SeparatingRight.toMatrix : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] {ι : Type u_6}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {B : LinearMap.BilinForm R₂ M₂},
  LinearMap.SeparatingRight B → ∀ (b : Module.Basis ι R₂ M₂), ((LinearMap.BilinForm.toMatrix b) B).SeparatingRight
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySum_isBounded : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (B : ℝ),
  Bornology.IsBounded (NumberField.mixedEmbedding.convexBodySum K B)
-- Mathlib.Algebra.FreeAlgebra
/-- `FreeAlgebra R X` has no zero-divisors when `R` has no zero-divisors.  -/
FreeAlgebra.instNoZeroDivisors : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R], NoZeroDivisors (FreeAlgebra R X)
-- Mathlib.CategoryTheory.Comma.Basic
/-- The functor `Comma L R ⥤ Comma L R` induced by the identity natural transformation on `L` is
naturally isomorphic to the identity functor.  -/
CategoryTheory.Comma.mapLeftId : {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) →
                CategoryTheory.Comma.mapLeft R (CategoryTheory.CategoryStruct.id L) ≅
                  CategoryTheory.Functor.id (CategoryTheory.Comma L R)
-- Mathlib.Analysis.Asymptotics.Theta
Filter.EventuallyEq.isTheta : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {l : Filter α} {f g : α → E}, f =ᶠ[l] g → f =Θ[l] g
-- Mathlib.Tactic.Translate.Core
_private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.applyReplacementFun.visitLambda : Mathlib.Tactic.Translate.TranslateData →
  Lean.Expr →
    List Lean.Expr →
      optParam (Array Lean.Expr) #[] → optParam Lean.LocalContext { } → Mathlib.Tactic.Translate.ReplacementM Lean.Expr
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.TextDocumentClientCapabilities.completion? : Lean.Lsp.TextDocumentClientCapabilities → Option Lean.Lsp.CompletionClientCapabilities
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.minKey!_modify_eq_minKey! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α] {k : α} {f : β → β}, (Std.DTreeMap.Const.modify t k f).minKey! = t.minKey!
-- Mathlib.Data.List.Defs
/-- Given a starting list `old`, a list of Booleans and a replacement list `new`,
read the items in `old` in succession and either replace them with the next element of `new` or
not, according as to whether the corresponding Boolean is `true` or `false`.  -/
List.replaceIf : {α : Type u_1} → List α → List Bool → List α → List α
-- Mathlib.RingTheory.Unramified.LocalStructure
Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
  [inst_3 : Q.IsPrime] [Algebra.FiniteType R S] [Algebra.IsUnramifiedAt R Q], ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
-- Mathlib.Algebra.Lie.Basic
/-- The inverse function of an equivalence of Lie algebras is a left inverse of the underlying
function.  -/
LieEquiv.left_inv : ∀ {R : Type u} {L : Type v} {L' : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (self : L ≃ₗ⁅R⁆ L'),
  Function.LeftInverse self.invFun (↑self.toLieHom).toFun
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.instInhabited : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [Inhabited C] → Inhabited (AlgebraicGeometry.PresheafedSpace C)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.skip?_bool_eq_some_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos res : s.Pos},
  pos.skip? p = some res ↔ ∃ (h : pos ≠ s.endPos), res = pos.next h ∧ p (pos.get h) = true
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.postcompIsoOfIso_hom_hom_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E] {A : Type u_5}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (F : CategoryTheory.SingleFunctors C D A) {G G' : CategoryTheory.Functor D E} (e : G ≅ G') [inst_6 : G.CommShift A]
  [inst_7 : G'.CommShift A] [inst_8 : CategoryTheory.NatTrans.CommShift e.hom A] (a : A) (X : C),
  ((F.postcompIsoOfIso e).hom.hom a).app X = e.hom.app ((F.functor a).obj X)
-- Mathlib.FieldTheory.Isaacs
IsAlgClosure.of_exists_root : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [alg : Algebra.IsAlgebraic F E],
  (∀ (p : Polynomial F), p.Monic → Irreducible p → ∃ x, (Polynomial.aeval x) p = 0) → IsAlgClosure F E
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.mk : {J : CategoryTheory.Limits.MulticospanShape} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (left : J.L → C) →
        (right : J.R → C) →
          ((b : J.R) → left (J.fst b) ⟶ right b) →
            ((b : J.R) → left (J.snd b) ⟶ right b) → CategoryTheory.Limits.MulticospanIndex J C
-- Init.Data.String.Basic
ByteArray.utf8Decode?.eq_1 : ∀ (b : ByteArray), b.utf8Decode? = ByteArray.utf8Decode?.go b 0 #[] ⋯
-- Mathlib.Control.Functor.Multivariate
MvFunctor.exists_iff_exists_of_mono : ∀ {n : ℕ} {α β : TypeVec.{u} n} (F : TypeVec.{u} n → Type v) [inst : MvFunctor F] [LawfulMvFunctor F] {P : F α → Prop}
  {q : F β → Prop} (f : α.Arrow β) (g : β.Arrow α),
  TypeVec.comp f g = TypeVec.id → (∀ (u : F α), P u ↔ q (MvFunctor.map f u)) → ((∃ u, P u) ↔ ∃ u, q u)
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.subRight_apply : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd Gᵃᵒᵖ G] (c b : G),
  (IsometryEquiv.subRight c) b = b - c
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.d_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  (d : M.Derivation φ) (X : Dᵒᵖ), d.d 1 = 0
-- Mathlib.Tactic.GCongr.Core
/-- Whether the order of the two varying arguments is the opposite from in the conclusion.  -/
Mathlib.Tactic.GCongr.GCongrHyp.isContra : Mathlib.Tactic.GCongr.GCongrHyp → Bool
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.submonoidComap_surjective_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (N' : Submonoid N),
  Function.Surjective ⇑f → Function.Surjective ⇑(f.submonoidComap N')
-- Init.Data.String.Basic
String.Pos.next.congr_simp : ∀ {s : String} (pos pos_1 : s.Pos) (e_pos : pos = pos_1) (h : pos ≠ s.endPos), pos.next h = pos_1.next ⋯
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The natural monoid hom from an `AddSubmonoid` of `AddMonoid` `M` to `M`.  -/
AddSubmonoidClass.subtype : {M : Type u_1} →
  {A : Type u_3} → [inst : AddZeroClass M] → [inst_1 : SetLike A M] → [hA : AddSubmonoidClass A M] → (S' : A) → ↥S' →+ M
-- Init.System.IOError
IO.Error.illegalOperation.sizeOf_spec : ∀ (osCode : UInt32) (details : String),
  sizeOf (IO.Error.illegalOperation osCode details) = 1 + sizeOf osCode + sizeOf details
-- Init.Data.UInt.Lemmas
UInt8.add_right_neg : ∀ (a : UInt8), a + -a = 0
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_eq_div_iff : ∀ {a b c d : ENNReal}, a ≠ 0 → a ≠ ⊤ → b ≠ 0 → b ≠ ⊤ → (c / b = d / a ↔ a * c = b * d)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instMonoidalMonMapAddMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : CategoryTheory.BraidedCategory C] →
                [inst_5 : CategoryTheory.BraidedCategory D] → [inst_6 : F.Braided] → F.mapAddMon.Monoidal
-- Mathlib.Analysis.InnerProductSpace.Laplacian
InnerProductSpace.laplacianWithin.congr_simp : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] (f f_1 : E → F),
  f = f_1 →
    ∀ (s s_1 : Set E),
      s = s_1 →
        ∀ (a a_1 : E), a = a_1 → InnerProductSpace.laplacianWithin f s a = InnerProductSpace.laplacianWithin f_1 s_1 a_1
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedMinOfIsClosedUnderIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) {Q : CategoryTheory.ObjectProperty C} [P.IsTriangulated] [Q.IsTriangulated]
  [Q.IsClosedUnderIsomorphisms], (P ⊓ Q).IsTriangulated
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.lsingle_apply : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (a : α) (b : M), (Finsupp.lsingle a) b = fun₀ | a => b
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.cancelMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : One M₁] [inst_2 : Pow M₁ ℕ] [inst_3 : CancelMonoid M₂]
  (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y)
  (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n),
  Function.Injective.cancelMonoid f hf one mul npow =
    { toLeftCancelMonoid := Function.Injective.leftCancelMonoid f hf one mul npow, toIsRightCancelMul := ⋯ }
-- Mathlib.Analysis.Fourier.Notation
FourierPair.fourierInv_fourier_eq : ∀ {E : Type u_5} {F : Type u_6} {inst : FourierTransform E F} {inst_1 : FourierTransformInv F E}
  [self : FourierPair E F] (f : E), FourierTransformInv.fourierInv (FourierTransform.fourier f) = f
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_zero : Complex.log 0 = 0
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerived_fac_assoc : ∀ {C : Type u_3} {D : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (RF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : RF.IsRightDerivedFunctor α W] (G : CategoryTheory.Functor D H) (β : F ⟶ L.comp G)
  {Z : CategoryTheory.Functor C H} (h : L.comp G ⟶ Z),
  CategoryTheory.CategoryStruct.comp α
      (CategoryTheory.CategoryStruct.comp (L.whiskerLeft (RF.rightDerivedDesc α W G β)) h) =
    CategoryTheory.CategoryStruct.comp β h
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.instIsDiscreteValuationRing : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], IsDiscreteValuationRing ℤ_[p]
-- Mathlib.Algebra.Group.Defs
DivInvMonoid.mk : {G : Type u} →
  [toMonoid : Monoid G] →
    [toInv : Inv G] →
      [toDiv : Div G] →
        [toZPow : ZPow G] →
          autoParam (∀ (a b : G), a / b = a * b⁻¹) DivInvMonoid.div_eq_mul_inv._autoParam →
            autoParam (∀ (a : G), a ^ 0 = 1) DivInvMonoid.zpow_zero'._autoParam →
              autoParam (∀ (n : ℕ) (a : G), a ^ ↑n.succ = a ^ ↑n * a) DivInvMonoid.zpow_succ'._autoParam →
                autoParam (∀ (n : ℕ) (a : G), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹) DivInvMonoid.zpow_neg'._autoParam →
                  DivInvMonoid G
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
CategoryTheory.PreservesImage.hom_comp_map_image_ι : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Limits.HasEqualizers A] [inst_3 : CategoryTheory.Limits.HasImages A]
  [inst_4 : CategoryTheory.StrongEpiCategory B] [inst_5 : CategoryTheory.Limits.HasImages B]
  (L : CategoryTheory.Functor A B)
  [inst_6 :
    ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L]
  [inst_7 :
    ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L]
  {X Y : A} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom
      (L.map (CategoryTheory.Limits.image.ι f)) =
    CategoryTheory.Limits.image.ι (L.map f)
-- Mathlib.Topology.Homeomorph.Lemmas
/-- A product of topological spaces can be split as the binary product of one of the spaces and
the product of all the remaining spaces.  -/
Homeomorph.piSplitAt : {ι : Type u_7} →
  [DecidableEq ι] →
    (i : ι) →
      (Y : ι → Type u_8) →
        [inst : (j : ι) → TopologicalSpace (Y j)] → ((j : ι) → Y j) ≃ₜ Y i × ((j : { j // j ≠ i }) → Y ↑j)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a b : α},
  cmp a b = Ordering.eq → t[a]? = t[b]?
-- Mathlib.Data.Sym.Basic
Sym.eq_nil_of_card_zero : ∀ {α : Type u_1} (s : Sym α 0), s = Sym.nil
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.preimage_mk_zero : ∀ {α : Type u_1} [inst : AddGroup α] (N : AddSubgroup α), QuotientAddGroup.mk ⁻¹' {↑0} = ↑N
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_roo : ∀ {α β : Type u} {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] [inst_4 : LT α]
  [inst_5 : DecidableLT α] [inst_6 : Std.PRange.UpwardEnumerable α] [inst_7 : Std.Rxo.IsAlwaysFinite α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerable α] [inst_9 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Roo α}
  {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.TreeMap.Raw.getEntryGED : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → α × β → α × β
-- Mathlib.GroupTheory.CommutingProbability
/-- A finite product of Dihedral groups.  -/
DihedralGroup.Product : List ℕ → Type
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If a binary fan `s` over `X Y` is a limit cone, then `s.swap` is a limit cone over `Y X`.  -/
CategoryTheory.Limits.IsLimit.binaryFanSwap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {s : CategoryTheory.Limits.BinaryFan X Y} → CategoryTheory.Limits.IsLimit s → CategoryTheory.Limits.IsLimit s.swap
-- Init.Data.Array.Lemmas
Array.append_ne_empty_of_left_ne_empty : ∀ {α : Type u_1} {xs ys : Array α}, xs ≠ #[] → xs ++ ys ≠ #[]
-- Mathlib.Data.Set.NAry
Set.image2_union_inter_subset_union : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t t' : Set β},
  Set.image2 f (s ∪ s') (t ∩ t') ⊆ Set.image2 f s t ∪ Set.image2 f s' t'
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_cyclesMap : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (β : CategoryTheory.ComposableArrows.mk₂ f₁ f₂ ⟶ CategoryTheory.ComposableArrows.mk₂ f₁' f₂'),
  β = CategoryTheory.ComposableArrows.homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯ →
    ∀ (n₀ n₁ n₂ : ℤ)
      (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_cyclesMap._auto_1)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_cyclesMap._auto_3),
      CategoryTheory.CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv
          (CategoryTheory.ShortComplex.cyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)) =
        CategoryTheory.CategoryStruct.comp (X.cyclesMap f₁ f₂ f₁' f₂' β n₁)
          (X.cyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).inv
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.key.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.key = 1
-- Mathlib.Algebra.Category.Grp.Yoneda
CommGrpCat.coyoneda_obj_obj_coe : ∀ (M : CommGrpCatᵒᵖ) (N : CommGrpCat), ↑((CommGrpCat.coyoneda.obj M).obj N) = (↑(Opposite.unop M) →* ↑N)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.Adjunction.homEquiv₂.eq_1 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {l : b ⟶ c} {r : c ⟶ b}
  (adj : CategoryTheory.Bicategory.Adjunction l r) {g : a ⟶ b} {h : a ⟶ c},
  adj.homEquiv₂ =
    {
      toFun := fun α =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft g adj.unit)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator g l r).inv
              (CategoryTheory.Bicategory.whiskerRight α r))),
      invFun := fun γ =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight γ l)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator h r l).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft h adj.counit)
              (CategoryTheory.Bicategory.rightUnitor h).hom)),
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yonedaEquiv_symm_naturality_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) {F F' : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
  (f : F ⟶ F') (x : F.obj (Opposite.op X)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.yonedaEquiv.symm x) f =
    CategoryTheory.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X))) x)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.comap_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (g : C(β, γ)) (f : C(α, β)),
  TopologicalSpace.Opens.comap (g.comp f) = (TopologicalSpace.Opens.comap f).comp (TopologicalSpace.Opens.comap g)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Equifibered.whiskerLeft : ∀ {J : Type u_1} {K : Type u_2} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] [inst_2 : CategoryTheory.Category.{v_3, u_2} K]
  {F G : CategoryTheory.Functor J C} {α : F ⟶ G},
  CategoryTheory.NatTrans.Equifibered α →
    ∀ (H : CategoryTheory.Functor K J), CategoryTheory.NatTrans.Equifibered (H.whiskerLeft α)
-- Mathlib.Data.Nat.Factors
Nat.prod_primeFactorsList : ∀ {n : ℕ}, n ≠ 0 → n.primeFactorsList.prod = n
-- Mathlib.Algebra.Group.WithOne.Defs
_private.Mathlib.Algebra.Group.WithOne.Defs.0.WithZero.unzero.match_1.splitter : {α : Type u_1} →
  (motive : (x : WithZero α) → x ≠ 0 → Sort u_2) →
    (x : WithZero α) → (x_1 : x ≠ 0) → ((x : α) → (x_2 : ↑x ≠ 0) → motive (some x) x_2) → motive x x_1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.inc.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (n : ℕ) (check persistent : Bool)
  (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_15) (fvarId_1 : Lean.FVarId)
  (n_1 : ℕ) (check_1 persistent_1 : Bool) (k_1 : Lean.Compiler.LCNF.Code pu)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_15),
  (Lean.Compiler.LCNF.Code.inc fvarId n check persistent k h =
      Lean.Compiler.LCNF.Code.inc fvarId_1 n_1 check_1 persistent_1 k_1 h_1) =
    (fvarId = fvarId_1 ∧ n = n_1 ∧ check = check_1 ∧ persistent = persistent_1 ∧ k = k_1)
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero : ∀ {n : ℕ} (hn : autoParam ({ len := n }.len ≤ 2) SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero._auto_1)
  (hn' : autoParam ({ len := n + 1 }.len ≤ 2) SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero._auto_3),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.δ₂ 1 hn hn') (SimplexCategory.Truncated.σ₂ 0 hn' hn) =
    CategoryTheory.CategoryStruct.id { obj := { len := n }, property := hn }
-- Mathlib.Topology.Algebra.Monoid
instContinuousAddULift : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M], ContinuousAdd (ULift.{u, u_3} M)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.unit : {α : outParam (Type u)} → {β : Type v} → [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] → Std.Sat.Literal α → β
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorZero_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (n : ℤ),
  ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.find?_eq_findSome? : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] [Std.Iterators.Finite α Id]
  {it : Std.Iter β} {f : β → Bool}, it.find? f = it.findSome? fun x => if f x = true then some x else none