mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- Extensionality lemma for morphisms from a module of the form `M₁ ⊗ (M₂ ⊗ M₃)`.  -/
SemimoduleCat.MonoidalCategory.tensor_ext₃ : ∀ {R : Type u} [inst : CommSemiring R] {M₁ M₂ M₃ M₄ : SemimoduleCat R}
  {f g :
    CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj M₂ M₃) ⟶ M₄},
  (∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃),
      (CategoryTheory.ConcreteCategory.hom f) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) =
        (CategoryTheory.ConcreteCategory.hom g) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃))) →
    f = g
-- Mathlib.Algebra.CharP.Lemmas
add_pow_char_pow : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (p n : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p],
  (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Algebra.IsIntegral.isField_iff_isField : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S] [IsDomain S], Function.Injective ⇑(algebraMap R S) → (IsField R ↔ IsField S)
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
MeasureTheory.integral_count : ∀ {X : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] [MeasurableSingletonClass X] [inst_4 : Fintype X] (f : X → E),
  ∫ (x : X), f x ∂MeasureTheory.Measure.count = ∑ a, f a
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- Manifolds with empty boundary are boundaryless.  -/
ModelWithCorners.Boundaryless.of_boundary_eq_empty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M], ModelWithCorners.boundary M = ∅ → BoundarylessManifold I M
-- Mathlib.Algebra.GroupWithZero.Associated
isUnit_of_associated_mul : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p b : M}, Associated (p * b) p → p ≠ 0 → IsUnit b
-- Init.Data.Array.Lemmas
Array.set_getElem_self : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size), xs.set i xs[i] h = xs
-- Mathlib.Data.ENat.Basic
ENat.succ_top : SuccOrder.succ ⊤ = ⊤
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.mulLeft_apply : ∀ (R : Type u_14) {A : Type u_15} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] (a b : A), (LinearMap.mulLeft R a) b = a * b
-- Lean.Declaration
Lean.OpaqueVal.mk.inj : ∀ {toConstantVal : Lean.ConstantVal} {value : Lean.Expr} {isUnsafe : Bool} {all : List Lean.Name}
  {toConstantVal_1 : Lean.ConstantVal} {value_1 : Lean.Expr} {isUnsafe_1 : Bool} {all_1 : List Lean.Name},
  { toConstantVal := toConstantVal, value := value, isUnsafe := isUnsafe, all := all } =
      { toConstantVal := toConstantVal_1, value := value_1, isUnsafe := isUnsafe_1, all := all_1 } →
    toConstantVal = toConstantVal_1 ∧ value = value_1 ∧ isUnsafe = isUnsafe_1 ∧ all = all_1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₂₁_single_inv_self_ρ_sub_self_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g : G) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ A))
      ((fun₀ | (g⁻¹, g) => (A.ρ g⁻¹) a) - fun₀ | (g, g⁻¹) => a) =
    (fun₀ | 1 => a) - fun₀ | 1 => (A.ρ g⁻¹) a
-- Init.Data.List.Sublist
List.filter_subset : ∀ {α : Type u_1} {l₁ l₂ : List α} (p : α → Bool), l₁ ⊆ l₂ → List.filter p l₁ ⊆ List.filter p l₂
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_two_mul : ∀ (x : ℂ), Complex.sin (2 * x) = 2 * Complex.sin x * Complex.cos x
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
/-- The additive action on an affine subspace corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.  -/
AffineSubspace.pointwiseVAdd : {k : Type u_2} →
  {V : Type u_3} →
    {P : Type u_4} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → VAdd V (AffineSubspace k P)
-- Mathlib.Logic.Equiv.Sum
Equiv.sigmaFiberEquiv_symm_apply_snd_coe : ∀ {α : Type u_9} {β : Type u_10} (f : α → β) (x : α), ↑((Equiv.sigmaFiberEquiv f).symm x).snd = x
-- Mathlib.Topology.Inseparable
SeparationQuotient.instIndiscreteTopologySubtype : ∀ {α : Type u_4} [inst : TopologicalSpace α] [IndiscreteTopology α] {p : α → Prop}, IndiscreteTopology (Subtype p)
-- Mathlib.Order.Filter.Pointwise
Filter.instSMul.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β],
  Filter.instSMul =
    {
      smul := fun f g =>
        let __src := Filter.map₂ (fun x1 x2 => x1 • x2) f g;
        { sets := {s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ • t₂ ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } }
-- Mathlib.Order.MinMax
le_min_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, c ≤ min a b ↔ c ≤ a ∧ c ≤ b
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.toSubgroup_ofSubgroup : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.Normal] [inst_2 : H.FiniteIndex],
  (FiniteIndexNormalSubgroup.ofSubgroup H).toSubgroup = H
-- Mathlib.Order.Antichain
/-- A strong (upward) antichain is a set such that no two distinct elements are related to a common
element.  -/
IsStrongAntichain : {α : Type u_1} → (α → α → Prop) → Set α → Prop
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.source_inter_preimage_target_inter : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set Y), e.source ∩ ↑e ⁻¹' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' s
-- Mathlib.Algebra.Notation.Support
Function.support_fun_zero : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M], (Function.support fun x => 0) = ∅
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
Std.Iter.atIdxSlow?_takeWhile : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Productive α Id] {l : ℕ} {it : Std.Iter β}
  {P : β → Bool},
  Std.Iter.atIdxSlow? l (Std.Iter.takeWhile P it) =
    if ∀ k ≤ l, Option.any P (Std.Iter.atIdxSlow? k it) = true then Std.Iter.atIdxSlow? l it else none
-- Mathlib.Probability.Process.FiniteDimensionalLaws
/-- The finite-dimensional distributions of a stochastic process are a projective measure family.  -/
ProbabilityTheory.isProjectiveMeasureFamily_map_restrict : ∀ {T : Type u_1} {Ω : Type u_2} {𝓧 : T → Type u_3} {mΩ : MeasurableSpace Ω} {mα : (t : T) → MeasurableSpace (𝓧 t)}
  {X : (t : T) → Ω → 𝓧 t} {P : MeasureTheory.Measure Ω},
  (∀ (t : T), AEMeasurable (X t) P) →
    MeasureTheory.IsProjectiveMeasureFamily fun I => MeasureTheory.Measure.map (fun ω => I.restrict fun x => X x ω) P
-- Mathlib.Order.Interval.Finset.Fin
Fin.attachFin_uIcc : ∀ {n : ℕ} (a b : Fin n), (Finset.uIcc ↑a ↑b).attachFin ⋯ = Finset.uIcc a b
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- The off-diagonal sums in Bird's equations (3) and (5) agree.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.paper_eq3_eq5_off_diag : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) {p : ℕ} (i j : Fin n),
  ∑ k > i, ∑ α ∈ BirdDet.S✝ p i, BirdDet.bminor✝ A i k α * A k j =
    ∑ α' ∈ BirdDet.S✝ (p + 1) i, ∑ t, BirdDet.bminor✝ A i (α' t) (t.removeNth α') * A (α' t) j
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.LocalizerMorphism.homMap_apply : ∀ {C₁ : Type u_2} {C₂ : Type u_3} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_2, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] [inst_2 : CategoryTheory.Category.{v_5, u_5} D₁]
  [inst_3 : CategoryTheory.Category.{v_6, u_6} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₂.IsLocalization W₂] {X Y : C₁} (G : CategoryTheory.Functor D₁ D₂) (e : Φ.functor.comp L₂ ≅ L₁.comp G)
  (f : L₁.obj X ⟶ L₁.obj Y),
  Φ.homMap L₁ L₂ f =
    CategoryTheory.CategoryStruct.comp (e.hom.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (e.inv.app Y))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.beq_iff_equiv : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α]
  [inst_1 : (k : α) → BEq (β k)] [∀ (k : α), LawfulBEq (β k)], (m₁ == m₂) = true ↔ m₁.Equiv m₂
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.rfl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α}, m.Equiv m
-- Std.Internal.UV.System
Std.Internal.UV.System.GroupInfo.mk : String → UInt64 → Array String → Std.Internal.UV.System.GroupInfo
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.EvalTacticFailure : Type
-- Aesop.RuleTac.Forward
Aesop.RuleTac.makeForwardHypProofs' : Lean.Expr → Option (Array Aesop.Substitution) → Aesop.UnorderedArraySet Aesop.PremiseIndex → Aesop.RuleTac.ForwardM Unit
-- Mathlib.Order.BooleanAlgebra.Set
Set.insert_sdiff_self_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → insert a (s \ {a}) = s
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.isLUB_l_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {s : Set α} {a : α}, IsLUB s a → IsLUB (l '' s) (l a)
-- Mathlib.Combinatorics.Graph.Delete
Graph.deleteVerts_le : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α}, G.deleteVerts X ≤ G
-- Mathlib.Data.Sym.Sym2
Sym2.diag.eq_1 : ∀ {α : Type u_1} (x : α), Sym2.diag x = s(x, x)
-- Init.Data.List.Attach
List.pmap_eq_map_attach : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} (H : ∀ a ∈ l, p a),
  List.pmap f l H = List.map (fun x => f ↑x ⋯) l.attach
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.mk.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] (a : M) (h : a ≠ 1),
  FiniteMulArchimedeanClass.mk a h = ⟨MulArchimedeanClass.mk a, ⋯⟩
-- Mathlib.Algebra.Vertex.HVertexOperator
HVertexOperator.coeff_apply_apply : ∀ {Γ : Type u_1} [inst : PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [inst_1 : CommRing R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddCommGroup W] [inst_5 : Module R W]
  (A : HVertexOperator Γ R V W) (n : Γ) (v : V), (HVertexOperator.coeff A n) v = ((HahnModule.of R).symm (A v)).coeff n
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a cone on `F.unop : J ⥤ C` into a cocone on `F : Jᵒᵖ ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.coconeOfConeUnop : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} → CategoryTheory.Limits.Cone F.unop → CategoryTheory.Limits.Cocone F
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.instEuclideanDomain : EuclideanDomain GaussianInt
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.instIsIsoHomHomCocone : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cocone F} (f : c ≅ d), CategoryTheory.IsIso f.inv.hom
-- Aesop.Forward.LevelIndex
Aesop.LevelIndex.mk : ℕ → Aesop.LevelIndex
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.coreToInt.injEq : ∀ (a b toIntThm : Lean.Expr) (lhs rhs : Int.Internal.Linear.Expr) (a_1 b_1 toIntThm_1 : Lean.Expr)
  (lhs_1 rhs_1 : Int.Internal.Linear.Expr),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.coreToInt a b toIntThm lhs rhs =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.coreToInt a_1 b_1 toIntThm_1 lhs_1 rhs_1) =
    (a = a_1 ∧ b = b_1 ∧ toIntThm = toIntThm_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableResolvableCompletionItem.hash : Lean.Lsp.ResolvableCompletionItem → UInt64
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.negMulLog_eq_neg : Real.negMulLog = fun x => -(x * Real.log x)
-- Mathlib.FieldTheory.KummerExtension
/-- Suppose `L/K` is the splitting field of `Xⁿ - a`, then a choice of `ⁿ√a` gives an equivalence of
`L` with `K[n√a]`.  -/
adjoinRootXPowSubCEquiv : {K : Type u} →
  [inst : Field K] →
    {n : ℕ} →
      {a : K} →
        {L : Type u_1} →
          [inst_1 : Field L] →
            [inst_2 : Algebra K L] →
              [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] →
                {α : L} →
                  (primitiveRoots n K).Nonempty →
                    Irreducible (Polynomial.X ^ n - Polynomial.C a) →
                      α ^ n = (algebraMap K L) a → AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] L
-- Init.Data.Int.Gcd
Int.gcd_ediv : ∀ {a b c : ℤ}, c ∣ a → c ∣ b → (a / c).gcd (b / c) = a.gcd b / c.natAbs
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
/-- Gluing `Iic a` and `Ioc a b` into `Iic b`. If `b < a`, this is just a projection on the first
coordinate followed by a restriction, see `IicProdIoc_le`.  -/
IicProdIoc : {ι : Type u_1} →
  [inst : LinearOrder ι] →
    [inst_1 : LocallyFiniteOrder ι] →
      [DecidableLE ι] →
        {X : ι → Type u_2} →
          [inst_3 : LocallyFiniteOrderBot ι] →
            (a b : ι) → ((i : ↥(Finset.Iic a)) → X ↑i) × ((i : ↥(Finset.Ioc a b)) → X ↑i) → (i : ↥(Finset.Iic b)) → X ↑i
-- Mathlib.Data.Finset.Sum
Finset.subset_map_inr : ∀ {α : Type u_1} {β : Type u_2} {t : Finset β} {u : Finset (α ⊕ β)},
  u ⊆ Finset.map Function.Embedding.inr t ↔ u.toLeft = ∅ ∧ u.toRight ⊆ t
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instCommRingUInt8 : Lean.Grind.CommRing UInt8
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- To construct an isomorphism of coalgebras, it suffices to give an isomorphism of the Vs which
commutes with the structure morphisms.
 -/
CategoryTheory.Endofunctor.Coalgebra.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} →
      {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} →
        (h : V₀.V ≅ V₁.V) →
          autoParam
              (CategoryTheory.CategoryStruct.comp V₀.str (F.map h.hom) =
                CategoryTheory.CategoryStruct.comp h.hom V₁.str)
              CategoryTheory.Endofunctor.Coalgebra.isoMk._auto_1 →
            (V₀ ≅ V₁)
-- Init.Data.Vector.Lemmas
Vector.reverse_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n), (Vector.mk xs h).reverse = Vector.mk xs.reverse ⋯
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.instMembership.eq_1 : ∀ {α : Type u_1}, FreeAddMonoid.instMembership = { mem := FreeAddMonoid.mem }
-- Mathlib.GroupTheory.Congruence.Defs
/-- The supremum of congruence relations `c, d` equals the smallest congruence relation containing
the binary relation '`x` is related to `y` by `c` or `d`'.  -/
Con.sup_eq_conGen : ∀ {M : Type u_1} [inst : Mul M] (c d : Con M), c ⊔ d = conGen fun x y => c x y ∨ d x y
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xn_modEq_x4n_sub : ∀ {a : ℕ} (a1 : 1 < a) {n j : ℕ}, j ≤ 2 * n → Pell.xn a1 (4 * n - j) ≡ Pell.xn a1 j [MOD Pell.xn a1 n]
-- Mathlib.Topology.Sets.Compacts
/-- The image of a compact set under a homeomorphism can also be expressed as a preimage.  -/
TopologicalSpace.Compacts.coe_equiv_apply_eq_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β)
  (K : TopologicalSpace.Compacts α), ↑((TopologicalSpace.Compacts.equiv f) K) = ⇑f.symm ⁻¹' ↑K
-- Mathlib.Analysis.Convex.Strict.Extreme
StrictConvexSpace.extremePoints_closedBall_eq_sphere : ∀ {A : Type u_1} [inst : NormedAddCommGroup A] [inst_1 : NormedSpace ℝ A] [Nontrivial A] {x : A} {r : ℝ}
  [StrictConvexSpace ℝ A], Set.extremePoints ℝ (Metric.closedBall x r) = Metric.sphere x r
-- Mathlib.Topology.Connected.LocallyConnected
/-- If each `X i` is locally connected and all but finitely many are preconnected, then
`∀ i, X i` is locally connected.  -/
Pi.locallyConnectedSpace_of_finite_not_preconnectedSpace : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), LocallyConnectedSpace (X i)],
  {i | ¬PreconnectedSpace (X i)}.Finite → LocallyConnectedSpace ((i : ι) → X i)
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.prevn : ∀ {l m₂ r m₁ : List Char} {s : Substring.Raw},
  Substring.Raw.ValidFor l (m₁.reverse ++ m₂) r s →
    ∀ (n : ℕ), s.prevn n { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len (List.drop n m₁) }
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv : ∀ {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₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv._auto_1),
  (X.cyclesIsoH f n₀ n₁ hn₁).inv = X.toCycles (CategoryTheory.CategoryStruct.id i₀) f f ⋯ n₀
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_map_eq_of_isUnit_leadingCoeff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] [Nontrivial S] (f : R →+* S),
  IsUnit p.leadingCoeff → (Polynomial.map f p).degree = p.degree
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.inhabited : Inhabited TopCat
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ioo_sub_one_left_eq_Ioc_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] {a : α},
  ¬IsMin a → ∀ (b : α), Set.Ioo (a - 1) b = Set.Ico a b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.pullbackAssoc_hom_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
      f₄]
  [inst_4 :
    CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom
      (CategoryTheory.Limits.pullback.fst f₁
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
      (CategoryTheory.Limits.pullback.fst f₁ f₂)
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.coe_id : ∀ {M : Type u_10} [inst : Zero M], ⇑(ZeroHom.id M) = id
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.monotone_u : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → Monotone u
-- Mathlib.GroupTheory.Coset.Basic
QuotientGroup.eq_class_eq_leftCoset : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) (g : α), {x | ↑x = ↑g} = g • ↑s
-- Mathlib.Analysis.Normed.Module.Basic
/-- The product of finitely many normed spaces is a normed space, with the sup norm.  -/
Pi.normedSpace : {𝕜 : Type u_1} →
  [inst : NormedField 𝕜] →
    {ι : Type u_6} →
      {E : ι → Type u_7} →
        [inst_1 : Fintype ι] →
          [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] →
            [(i : ι) → NormedSpace 𝕜 (E i)] → NormedSpace 𝕜 ((i : ι) → E i)
-- Lean.Parser.Basic
Lean.Parser.instBEqRecoveryContext.beq : Lean.Parser.RecoveryContext → Lean.Parser.RecoveryContext → Bool
-- Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
/-- If `0 ∉ S`, then every chain in `kaplanskySet S` has an upper bound.  -/
_private.Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky.0.UniqueFactorizationMonoid.exists_mem_kaplanskySet_le : ∀ {R : Type u_1} [inst : Semiring R] {S : Subsemigroup R} {C : Set (Ideal R)},
  0 ∉ S →
    C ⊆ UniqueFactorizationMonoid.kaplanskySet✝ S →
      IsChain (fun x1 x2 => x1 ≤ x2) C → ∃ P ∈ UniqueFactorizationMonoid.kaplanskySet✝ S, ∀ J ∈ C, J ≤ P
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.documentHighlightProvider : Lean.Lsp.ServerCapabilities → Bool
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Constructing an affine subspace from a point in a subspace and that subspace's direction
yields the original subspace.  -/
AffineSubspace.mk'_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p : P}, p ∈ s → AffineSubspace.mk' p s.direction = s
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instBEqExpect.beq : Std.Http.Header.Expect → Std.Http.Header.Expect → Bool
-- Init.Data.Bool
Bool.le_of_lt : ∀ {x y : Bool}, x < y → x ≤ y
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ D` creates colimits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F.rightOp : C ⥤ Dᵒᵖ` creates
limits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.createsLimitRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor Cᵒᵖ D) →
                [CategoryTheory.CreatesColimit K.op F] → CategoryTheory.CreatesLimit K F.rightOp
-- Init.Data.Int.Gcd
Int.lcm_mul_left : ∀ (m n k : ℤ), (m * n).lcm (m * k) = m.natAbs * n.lcm k
-- Mathlib.Analysis.Convex.EGauge
egauge_lt_iff : ∀ {𝕜 : Type u_1} [inst : NNNorm 𝕜] {E : Type u_2} [inst_1 : SMul 𝕜 E] {s : Set E} {x : E} {r : ENNReal},
  egauge 𝕜 s x < r ↔ ∃ c, x ∈ c • s ∧ ‖c‖ₑ < r
-- Lean.MetavarContext
/-- `isDefEq` avoids assignment  -/
Lean.MetavarKind.synthetic : Lean.MetavarKind
-- Mathlib.Tactic.Recall
/-- Format a `recall` suggestion string for the given constant name.
Uses `delabConstWithSignature` with `universes := false` to produce the idiomatic
decomposed binder form without universe parameters on the name.  -/
_private.Mathlib.Tactic.Recall.0.Mathlib.Tactic.Recall.mkRecallSuggestion : Lean.Name → Lean.MetaM String
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.complex_exp_eq_normedSpace_exp : ∀ {A : Type u_1} {p : A → Prop} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℂ A]
  [inst_3 : ContinuousFunctionalCalculus ℂ A p] {a : A},
  autoParam (p a) CFC.complex_exp_eq_normedSpace_exp._auto_1 → cfc Complex.exp a = NormedSpace.exp a
-- Lean.PrivateName
Lean.privateToUserName? : Lean.Name → Option Lean.Name
-- Mathlib.Analysis.InnerProductSpace.Calculus
contDiff_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {n : WithTop ℕ∞}, ContDiff ℝ n fun p => inner 𝕜 p.1 p.2
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.MeasurePreserving.setIntegral_preimage_emb : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure X} {Y : Type u_5} {x : MeasurableSpace Y} {f : X → Y} {ν : MeasureTheory.Measure Y},
  MeasureTheory.MeasurePreserving f μ ν →
    MeasurableEmbedding f → ∀ (g : Y → E) (s : Set Y), ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ = ∫ (y : Y) in s, g y ∂ν
-- Mathlib.Algebra.NoZeroSMulDivisors.Defs
NoZeroSMulDivisors.mk : ∀ {R : Type u_4} {M : Type u_5} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMul R M],
  (∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0) → NoZeroSMulDivisors R M
-- Init.Data.SInt.Basic
/-- Bitwise exclusive or for word-sized signed integers. Usually accessed via the `^^^` operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of the input
integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.xor : ISize → ISize → ISize
-- Mathlib.Data.Complex.Basic
Complex.div_intCast_re : ∀ (z : ℂ) (n : ℤ), (z / ↑n).re = z.re / ↑n