mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- For `h : S.LeftHomologyData`, this is a restatement of `h.hπ`, saying that
`π : h.K ⟶ h.H` is a cokernel of `h.f' : S.X₁ ⟶ h.K`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.hπ' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.LeftHomologyData) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ h.π ⋯)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.eval₂_T : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_3} [inst_1 : CommSemiring S] (f : R →+* S) (x : Sˣ) (n : ℤ),
  (LaurentPolynomial.eval₂ f x) (LaurentPolynomial.T n) = ↑(x ^ n)
-- Mathlib.Topology.Algebra.SeparationQuotient.Section
/-- A continuous `K`-linear map from `SeparationQuotient E` to `E`
such that `mk (outCLM x) = x` for all `x`.  -/
SeparationQuotient.outCLM : (K : Type u_1) →
  (E : Type u_2) →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module K E] →
          [inst_3 : TopologicalSpace E] →
            [inst_4 : IsTopologicalAddGroup E] → [inst_5 : ContinuousConstSMul K E] → SeparationQuotient E →L[K] E
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agmSequences_fst_lt_snd_of_ne : ∀ {x y : NNReal}, x ≠ y → ∀ (n m : ℕ), (x.agmSequences y n).1 < (x.agmSequences y m).2
-- Init.Data.Option.Lemmas
Option.self_beq_filter : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α] {p : α → Bool} {o : Option α}, (o == Option.filter p o) = Option.all p o
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
ExteriorAlgebra.basis_mul_of_disjoint : ∀ {R : Type u_1} {M : Type u_2} {m n : ℕ} {I : Type u_3} [inst : LinearOrder I] [inst_1 : CommRing R]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I m))
  (t : ↑(Set.powersetCard I n)) (h : Disjoint ↑s ↑t),
  b.ExteriorAlgebra ↑s * b.ExteriorAlgebra ↑t =
    Equiv.Perm.sign (Set.powersetCard.permOfDisjoint h) • b.ExteriorAlgebra ↑(Set.powersetCard.disjUnion h)
-- Mathlib.Algebra.Group.Semiconj.Units
SemiconjBy.units_val : ∀ {M : Type u_1} [inst : Monoid M] {a x y : Mˣ}, SemiconjBy a x y → SemiconjBy ↑a ↑x ↑y
-- Mathlib.Topology.Homeomorph.Defs
Equiv.toEquiv_toHomeomorphOfIsInducing : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X ≃ Y)
  (hf : Topology.IsInducing ⇑f), (f.toHomeomorphOfIsInducing hf).toEquiv = f
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {x y : α},
  x ≠ 0 →
    y ≠ 0 →
      (DvdNotUnit x y ↔ UniqueFactorizationMonoid.normalizedFactors x < UniqueFactorizationMonoid.normalizedFactors y)
-- Std.Http.Internal.Encode
Std.Http.Internal.Encode.mk : {v : Std.Http.Version} →
  {t : Type} → (Std.Http.Internal.ChunkedBuffer → t → Std.Http.Internal.ChunkedBuffer) → Std.Http.Internal.Encode v t
-- Mathlib.Topology.ContinuousMap.Defs
/-- The type of continuous maps from `X` to `Y`.

When possible, instead of parametrizing results over `(f : C(X, Y))`,
you should parametrize over `{F : Type*} [ContinuousMapClass F X Y] (f : F)`.

When you extend this structure, make sure to extend `ContinuousMapClass`.  -/
ContinuousMap : (X : Type u_1) → (Y : Type u_2) → [TopologicalSpace X] → [TopologicalSpace Y] → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.BinaryBicone.ofLimitCone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)} (ht : CategoryTheory.Limits.IsLimit t),
  (CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).pt = t.pt
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeffAddEquiv_symm_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (coeff : ℕ →₀ M),
  PolynomialModule.coeffAddEquiv.symm coeff = { coeff := coeff }
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- Note: this assumes `[IsLeftUniformGroup β] [IsRightUniformGroup β]` instead of the more typical
(and equivalent) `[IsUniformGroup β]` because this is used in the proof of said equivalence.  -/
comap_conj_nhds_one : ∀ {β : Type u_2} [inst : UniformSpace β] [inst_1 : Group β] [IsLeftUniformGroup β] [IsRightUniformGroup β],
  Filter.comap (fun gx => gx.1 * gx.2 * gx.1⁻¹) (nhds 1) = Filter.comap Prod.snd (nhds 1)
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.InducedCategory.homLinearEquiv_symm_apply_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type w}
  [inst_2 : Semiring R] [inst_3 : CategoryTheory.Linear R C] {D : Type u'} {F : D → C}
  {X Y : CategoryTheory.InducedCategory C F} (a : F X ⟶ F Y),
  (CategoryTheory.InducedCategory.homLinearEquiv.symm a).hom = a
-- Init.Data.Nat.Coprime
Nat.coprime_self : ∀ (n : ℕ), n.Coprime n ↔ n = 1
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
Set.Iic_ciInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α},
  BddBelow (Set.range f) → Set.Iic (⨅ i, f i) = ⋂ i, Set.Iic (f i)
-- Mathlib.Order.Filter.Basic
/-- Eta-expanded form of `Filter.EventuallyEq.sub` -/
Filter.EventuallyEq.fun_sub : ∀ {α : Type u} {β : Type v} [inst : Sub β] {f f' g g' : α → β} {l : Filter α},
  f =ᶠ[l] g → f' =ᶠ[l] g' → (fun i => f i - f' i) =ᶠ[l] fun i => g i - g' i
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.brecOn_2.go : {α : Type u} →
  {β : Type v} →
    {motive_1 : Lean.PersistentHashMap.Node α β → Sort u_1} →
      {motive_2 : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1} →
        {motive_3 : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1} →
          {motive_4 : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_1} →
            (t : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
              ((t : Lean.PersistentHashMap.Node α β) → t.below → motive_1 t) →
                ((t : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
                    Lean.PersistentHashMap.Node.below_1 t → motive_2 t) →
                  ((t : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
                      Lean.PersistentHashMap.Node.below_2 t → motive_3 t) →
                    ((t : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) →
                        Lean.PersistentHashMap.Node.below_3 t → motive_4 t) →
                      motive_3 t ×' Lean.PersistentHashMap.Node.below_2 t
-- Mathlib.Order.Defs.Unbundled
Std.Total.decide : ∀ {α : Sort u_1} {r : α → α → Prop} [inst : DecidableRel r] [Std.Total r], Std.Total fun a b => decide (r a b) = true
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.disjointOfDiff.congr_simp : ∀ {α : Type u_1} {C C_1 : Set (Set α)} (e_C : C = C_1) {s s_1 : Set α} (e_s : s = s_1) {t t_1 : Set α} (e_t : t = t_1)
  (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C), hC.disjointOfDiff hs ht = ⋯.disjointOfDiff ⋯ ⋯
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Comma.costructuredArrowSndInclusion_map : ∀ {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) (b : B) {X Y : CategoryTheory.CostructuredArrow L (R.obj b)} (f : X ⟶ Y),
  (CategoryTheory.Comma.costructuredArrowSndInclusion L R b).map f =
    CategoryTheory.CostructuredArrow.homMk { left := f.left, right := CategoryTheory.CategoryStruct.id b, w := ⋯ } ⋯
-- Lean.Data.Json.FromToJson.Basic
Lean.USize.fromJson? : Lean.Json → Except String USize
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.exists_integral_multiple : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {z : A},
  IsAlgebraic R z → ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)
-- Mathlib.Data.Finsupp.Basic
Finsupp.coe_curryAddEquiv : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddZeroClass M], ⇑Finsupp.curryAddEquiv = Finsupp.curry
-- Mathlib.Data.Nat.Choose.Factorization
/-- Primes greater than about `sqrt n` appear only to multiplicity 0 or 1
in the binomial coefficient.  -/
Nat.factorization_choose_le_one : ∀ {p n k : ℕ}, n < p ^ 2 → (n.choose k).factorization p ≤ 1
-- Init.Simproc
/-- Similar to `simproc`, but resulting expression must be definitionally equal to the input one.
 -/
Lean.Parser.«command__Dsimproc__[_]_(_):=_» : Lean.ParserDescr
-- Init.Data.Fin.Basic
Fin.zero_eta : ∀ {n : ℕ}, ⟨0, ⋯⟩ = 0
-- Init.Data.String.Basic
/-- Advances a valid position on a slice to the next valid position, or panics if the given
position is the past-the-end position.  -/
String.Slice.Pos.next! : {s : String.Slice} → s.Pos → s.Pos
-- Mathlib.Data.Set.Restrict
Set.surjOn_iff_surjective : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.SurjOn f s Set.univ ↔ Function.Surjective (s.domRestrict f)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- The underlying `Cofork` of a `ReflexiveCofork`.  -/
CategoryTheory.Limits.ReflexiveCofork.toCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C} →
      CategoryTheory.Limits.ReflexiveCofork F →
        CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
          (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- The Gram-Schmidt process takes a set of vectors as input
and outputs a set of orthogonal vectors which have the same span.  -/
InnerProductSpace.gramSchmidt : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [InnerProductSpace 𝕜 E] →
          {ι : Type u_3} → [inst : LinearOrder ι] → [LocallyFiniteOrderBot ι] → [WellFoundedLT ι] → (ι → E) → ι → E
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivWithinAt.sum : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {s : Set M} {z : M} {ι : Type} {t : Finset ι} {f : ι → M → E'}
  {f' : ι → TangentSpace I z →L[𝕜] E'},
  (∀ i ∈ t, HasMFDerivAt[s] (f i) z (f' i)) → HasMFDerivAt[s] (∑ i ∈ t, f i) z (∑ i ∈ t, f' i)
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Limits.limitCompCoyonedaIsoCone_inv : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) (X : C),
  (CategoryTheory.Limits.limitCompCoyonedaIsoCone F X).inv =
    TypeCat.ofHom fun t =>
      (CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.limit.lift (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X)))
            (CategoryTheory.Limits.Types.coneOfSection ⋯)))
        PUnit.unit
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.preimage_inv : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveInv α] (s : Finset α), s.preimage (fun x => x⁻¹) ⋯ = s⁻¹
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isLimitConeOfCoconeRightOp_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F.rightOp}
  (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.isLimitConeOfCoconeRightOp F hc).lift s =
    (hc.desc (CategoryTheory.Limits.coconeRightOpOfCone s)).unop
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialRightAdjointHomEquiv_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : F.PartialRightAdjointSource} (f : X ⟶ Y),
  F.partialRightAdjointHomEquiv (F.partialRightAdjointMap f) =
    CategoryTheory.CategoryStruct.comp
      (F.partialRightAdjointHomEquiv (CategoryTheory.CategoryStruct.id (F.partialRightAdjointObj X))) f.hom
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.instEmptyCollection : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → EmptyCollection (Std.ExtDHashMap α β)
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncateFun_zsmul : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (m : ℤ) (x : WittVector p R),
  WittVector.truncateFun n (m • x) = m • WittVector.truncateFun n x
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.lift_fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.lift F') (CategoryTheory.CategoryStruct.comp F'.m h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.u.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] (x x_1 : E),
  x = x_1 → ExistsContDiffBumpBase.u x = ExistsContDiffBumpBase.u x_1
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.TreeMap.get! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited β] → Std.TreeMap α β cmp → α → β
-- Lean.Data.Options
Lean.Option.register : {α : Type} →
  [Lean.KVMap.Value α] →
    Lean.Name → Lean.Option.Decl α → autoParam Lean.Name Lean.Option.register._auto_1 → IO (Lean.Option α)
-- Init.Data.Option.Lemmas
Option.ne_none_iff_isSome : ∀ {α : Type u_1} {o : Option α}, o ≠ none ↔ o.isSome = true
-- Mathlib.Order.RelClasses
Set.not_bounded_iff : ∀ {α : Type u} {r : α → α → Prop} (s : Set α), ¬Set.Bounded r s ↔ Set.Unbounded r s
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.prodPrimeFactors_apply : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {f : ℕ → R} {n : ℕ},
  n ≠ 0 → (ArithmeticFunction.prodPrimeFactors fun p => f p) n = ∏ p ∈ n.primeFactors, f p
-- Init.Grind.AC
Lean.Grind.AC.eq_norm_aci_cert : Lean.Grind.AC.Expr → Lean.Grind.AC.Expr → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.writtenInCharts : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAtOfComplement F I J n f x),
  Set.EqOn (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm) (⇑h.equiv ∘ fun x => (x, 0))
    (h.domChart.extend I).target
-- Init.Omega.IntList
/-- Implementation of `+` on `IntList`.  -/
Lean.Omega.IntList.add : Lean.Omega.IntList → Lean.Omega.IntList → Lean.Omega.IntList
-- Mathlib.NumberTheory.FunctionField
FunctionField.FiniteDimensional.adjoin_algebraMap_X : ∀ {F : Type u_3} {K : Type u_4} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (RatFunc F) K] [FunctionField F K]
  [inst_4 : Algebra F K] [IsScalarTower F (RatFunc F) K], FiniteDimensional (↥F⟮(algebraMap (RatFunc F) K) RatFunc.X⟯) K
-- Mathlib.RingTheory.SimpleModule.Basic
LinearEquiv.isSimpleModule_iff : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : M ≃ₗ[R] N), IsSimpleModule R M ↔ IsSimpleModule R N
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_ofNat : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (n : ℕ) [inst_1 : n.AtLeastTwo], (OfNat.ofNat n).imK = 0
-- Init.Data.Vector.Lemmas
Vector.prod_reverse : ∀ {α : Type u_1} {n : ℕ} [inst : One α] [inst_1 : Mul α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.Commutative fun x1 x2 => x1 * x2] [Std.LawfulLeftIdentity (fun x1 x2 => x1 * x2) 1] (xs : Vector α n),
  xs.reverse.prod = xs.prod
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabRange : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.pageFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  (c : ℤ → ComplexShape κ) (r₀ r : ℤ) (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.pageFunctor._auto_1)
  (E : CategoryTheory.SpectralSequence C c r₀),
  (CategoryTheory.SpectralSequence.pageFunctor C c r₀ r hr).obj E = E.page r ⋯
-- Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
/-- The special adjoint functor theorem: if `G : D ⥤ C` preserves limits and `D` is complete,
well-powered and has a small coseparating set, then `G` has a left adjoint.
 -/
CategoryTheory.isRightAdjoint_of_preservesLimits_of_isCoseparating : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} D]
  [CategoryTheory.Limits.HasLimits D] [CategoryTheory.WellPowered.{v, v, u'} D] {P : CategoryTheory.ObjectProperty D}
  [CategoryTheory.ObjectProperty.Small.{v, v, u'} P],
  P.IsCoseparating → ∀ (G : CategoryTheory.Functor D C) [CategoryTheory.Limits.PreservesLimits G], G.IsRightAdjoint
-- Mathlib.Algebra.GroupWithZero.InjSurj
Function.Injective.isCancelMulZero : ∀ {M₀ : Type u_1} {M₀' : Type u_3} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : Mul M₀'] [inst_3 : Zero M₀']
  (f : M₀ → M₀'),
  Function.Injective f → f 0 = 0 → (∀ (x y : M₀), f (x * y) = f x * f y) → ∀ [IsCancelMulZero M₀'], IsCancelMulZero M₀
-- Lean.Level
Lean.Level.PP.Result : Type
-- Mathlib.Algebra.Group.NatPowAssoc
Pi.instNatPowAssoc : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → MulOneClass (α i)] [inst_1 : (i : ι) → Pow (α i) ℕ]
  [∀ (i : ι), NatPowAssoc (α i)], NatPowAssoc ((i : ι) → α i)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- All points have distance to the circumcenter equal to the
circumradius.  -/
Affine.Simplex.dist_circumcenter_eq_circumradius' : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  dist s.circumcenter (s.points i) = s.circumradius
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.prehaar_nonneg : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G}
  (K : TopologicalSpace.Compacts G), 0 ≤ MeasureTheory.Measure.haar.prehaar (↑K₀) U K
-- Mathlib.Data.Finset.Defs
Finset.Superset.trans : ∀ {α : Type u_1} {s₁ s₂ s₃ : Finset α}, s₁ ⊇ s₂ → s₂ ⊇ s₃ → s₁ ⊇ s₃
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqMon.beq_spec_1 : (Lean.Grind.CommRing.Mon.unit == Lean.Grind.CommRing.Mon.unit) = true
-- Mathlib.Data.Fintype.BigOperators
Fintype.prod_dite : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] {p : α → Prop} [inst_1 : DecidablePred p] [inst_2 : CommMonoid β]
  (f : (a : α) → p a → β) (g : (a : α) → ¬p a → β), ∏ a, dite (p a) (f a) (g a) = (∏ a, f ↑a ⋯) * ∏ a, g ↑a ⋯
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
/-- The usual sheaf condition can be obtained from the sheaf condition
in terms of unique gluings.
 -/
TopCat.Presheaf.isSheaf_of_isSheafUniqueGluing_types : ∀ {X : TopCat} (F : TopCat.Presheaf (Type u_4) X), F.IsSheafUniqueGluing → F.IsSheaf
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.card_eq : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Fintype α], Fintype.card (AddChar α ℂ) = Fintype.card α
-- Mathlib.Order.Basic
eq_of_le_of_not_lt : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≤ b → ¬a < b → a = b
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.measure_add_measure_eq : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G]
  (μ' ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν']
  [μ'.IsAddLeftInvariant] [ν'.IsAddLeftInvariant] (s t : Set G), ν' s ≠ 0 → ν' s ≠ ⊤ → μ' s * ν' t = ν' s * μ' t
-- Mathlib.LinearAlgebra.UnitaryGroup
/-- The kronecker product of two unitary matrices is unitary.

This is stated for `unitary` instead of `unitaryGroup` as it holds even for
non-commutative coefficients.  -/
Matrix.kronecker_mem_unitary : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_1} {m : Type u_2} [inst_2 : Semiring R]
  [inst_3 : StarRing R] [inst_4 : Fintype m] [inst_5 : DecidableEq m] {U₁ : Matrix n n R} {U₂ : Matrix m m R},
  U₁ ∈ unitary (Matrix n n R) →
    U₂ ∈ unitary (Matrix m m R) → Matrix.kroneckerMap (fun x1 x2 => x1 * x2) U₁ U₂ ∈ unitary (Matrix (n × m) (n × m) R)
-- Mathlib.Topology.Semicontinuity.Basic
/-- An intersection of overlevel sets of a lower semicontinuous function
on a compact set is empty if and only if a finite sub-intersection is already empty.  -/
UpperSemicontinuousOn.inter_biInter_preimage_Ici_eq_empty_iff_exists_finset : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ] {ι : Type u_5}
  {f : ι → α → γ},
  IsCompact s →
    ∀ {I : Set ι} {c : γ},
      (∀ i ∈ I, UpperSemicontinuousOn (f i) s) →
        (s ∩ ⋂ i ∈ I, f i ⁻¹' Set.Ici c = ∅ ↔ ∃ u, ∀ x ∈ s, ∃ i ∈ u, f (↑i) x < c)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.desc.multicofork_π_two_assoc : ∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃)
  {Z : SSet} (h : (SSet.horn₃₁.desc.multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((SSet.horn₃₁.desc.multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π ⟨2, SSet.horn₃₁.desc.multicofork_π_two._proof_1⟩) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso 2).inv f₂) h
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- Let `F` be a homotopy between two continuous maps `f g : C(X, Y)`.
Given a path `p : Path x₁ x₂` in the domain, consider the following two paths in the codomain.
One path goes along the image of `p` under `f`, then along the trajectory of `x₂` under `F`.
The other path goes along the trajectory of `x₁` under `F`, then along the image of `p` under `g`.

These two paths are homotopic.  -/
Path.Homotopic.map_trans_evalAt : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f g : C(X, Y)}
  (F : f.Homotopy g) {x₁ x₂ : X} (p : Path x₁ x₂),
  ((p.map ⋯).trans (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))