mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) {Y Z : C}
  (f : X ⟶ Z) (g : Y ⟶ Z) [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.f i) f) g]
  (i : E.I₀),
  (E.pullbackCoverOfLeft f g).f i =
    CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (E.f i) f) g f g (E.f i)
      (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯
-- Mathlib.GroupTheory.Nilpotent
/-- Groups with nilpotency class at most one are abelian.  -/
commGroupOfNilpotencyClass : {G : Type u_1} → [inst : Group G] → [Group.IsNilpotent G] → Group.nilpotencyClass G ≤ 1 → CommGroup G
-- Mathlib.Analysis.Normed.Group.Basic
mem_sphere_iff_norm : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a b : E} {r : ℝ}, b ∈ Metric.sphere a r ↔ ‖b - a‖ = r
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- the functor preserves the kernel of `S.g : S.X₂ ⟶ S.X₃`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.g : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C}
  {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData)
  {F : CategoryTheory.Functor C D} {inst_4 : F.PreservesZeroMorphisms} [self : h.IsPreservedBy F],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.pow_cpow_ofNat_inv : ∀ {x : ℂ} {n : ℕ} [inst : n.AtLeastTwo],
  -(Real.pi / OfNat.ofNat n) < x.arg → x.arg ≤ Real.pi / OfNat.ofNat n → (x ^ OfNat.ofNat n) ^ (OfNat.ofNat n)⁻¹ = x
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.partitionWithPartEquiv_symm_apply_parts : ∀ {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n) (p : (n - a).Partition),
  (↑((Nat.Partition.partitionWithPartEquiv ha1 ha).symm p)).parts = a ::ₘ p.parts
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.JPDecl.body : Lean.Elab.Term.Do.JPDecl → Lean.Elab.Term.Do.Code
-- Std.Data.TreeMap.Raw.Lemmas
/-- Simpler variant of `getElem?_filterMap` when `LawfulEqCmp` is available.  -/
Std.TreeMap.Raw.getElem?_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α},
  t.WF → (Std.TreeMap.Raw.filterMap f t)[k]? = t[k]?.bind fun x => f k x
-- Mathlib.Data.Fintype.Card
Fintype.card_ulift : ∀ (α : Type u_4) [inst : Fintype α], Fintype.card (ULift.{u_5, u_4} α) = Fintype.card α
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.valuation_intCast : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℤ), (↑n).valuation = ↑(padicValInt p n)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.locallySmall_of_isLocalization : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] (L : CategoryTheory.Functor C D)
  [L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] [CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.LocallySmall.{w, v_1, u_1} D
-- Mathlib.CategoryTheory.Monad.Limits
/-- If `C` has colimits then any coreflective subcategory has colimits.  -/
CategoryTheory.hasColimits_of_coreflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (R : CategoryTheory.Functor D C) [CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₁, u₁} C]
  [CategoryTheory.Coreflective R], CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₂, u₂} D
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.mul_adjugate_apply : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  (i j k : n), A i k * A.adjugate k j = A.transpose.cramer (Pi.single k (A i k)) j
-- Mathlib.Order.GameAdd
/-- Induction on the well-founded `Prod.GameAdd` relation.
Note that it's strictly more general to induct on the lexicographic order instead.  -/
Prod.GameAdd.induction : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {C : α → β → Prop},
  WellFounded rα →
    WellFounded rβ →
      (∀ (a₁ : α) (b₁ : β), (∀ (a₂ : α) (b₂ : β), Prod.GameAdd rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁) →
        ∀ (a : α) (b : β), C a b
-- Mathlib.Order.Monotone.Defs
strictMono_id : ∀ {α : Type u} [inst : Preorder α], StrictMono id
-- Mathlib.Order.UpperLower.Basic
isLowerSet_sInter : ∀ {α : Type u_1} [inst : LE α] {S : Set (Set α)}, (∀ s ∈ S, IsLowerSet s) → IsLowerSet (⋂₀ S)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_comp_polynomial : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p]
  [ContinuousMap.UniqueHom R A] (q : Polynomial R) (f : R → R) (a : A),
  autoParam (ContinuousOn f ((fun x => Polynomial.eval x q) '' spectrum R a)) cfc_comp_polynomial._auto_1 →
    autoParam (p a) cfc_comp_polynomial._auto_3 →
      cfc (fun x => f (Polynomial.eval x q)) a = cfc f ((Polynomial.aeval a) q)
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-Noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).


[Stacks Tag 09G3](https://stacks.math.columbia.edu/tag/09G3) (first part) -/
Module.rank : (R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Cardinal.{u_2}
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.PreservesZeroMorphisms.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {F : CategoryTheory.Functor C D},
  autoParam (∀ (X Y : C), F.map 0 = 0) CategoryTheory.Functor.PreservesZeroMorphisms.map_zero._autoParam →
    F.PreservesZeroMorphisms
-- Mathlib.Order.Hom.Bounded
BotHom.instMin : {α : Type u_2} →
  {β : Type u_3} → [inst : Bot α] → [inst_1 : SemilatticeInf β] → [inst_2 : OrderBot β] → Min (BotHom α β)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.instEpiSnd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y], CategoryTheory.Epi (CategoryTheory.Limits.coprod.snd X Y)
-- Mathlib.RingTheory.ChainOfDivisors
pow_image_of_prime_by_factor_orderIso_dvd : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [inst_2 : CommMonoidWithZero N]
  [UniqueFactorizationMonoid N] [inst_4 : UniqueFactorizationMonoid M] {m p : Associates M} {n : Associates N},
  n ≠ 0 →
    ∀ (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)) {s : ℕ},
      p ^ s ≤ m → ↑(d ⟨p, ⋯⟩) ^ s ≤ n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.map_dblX : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).dblX (⇑f ∘ P) = f (W'.dblX P)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_alter_eq_self_of_mem : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      m.contains k = true → (f (m.get? k)).isSome = true → (↑(m.alter k f)).size = (↑m).size
-- Mathlib.Data.Fintype.Sets
mem_image_univ_iff_mem_range : ∀ {α : Type u_4} {β : Type u_5} [inst : Fintype α] [inst_1 : DecidableEq β] {f : α → β} {b : β},
  b ∈ Finset.image f Finset.univ ↔ b ∈ Set.range f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasStrictDerivAt.cos : ∀ {f : ℝ → ℝ} {f' x : ℝ}, HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) * f') x
-- Mathlib.CategoryTheory.Abelian.Preradical.Radical
CategoryTheory.Abelian.Preradical.isRadical_iff_isIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C),
  CategoryTheory.Abelian.Preradical.isRadical C Φ ↔ CategoryTheory.IsIso (Φ.toColon Φ)
-- Mathlib.CategoryTheory.Core
/-- Taking the core of a functor is functorial if we discard non-invertible natural
transformations.  -/
CategoryTheory.coreFunctor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor (CategoryTheory.Core (CategoryTheory.Functor C D))
          (CategoryTheory.Functor (CategoryTheory.Core C) (CategoryTheory.Core D))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
PresheafOfModules.instFaithfulRestrictScalars : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R ⟶ R'),
  (PresheafOfModules.restrictScalars α).Faithful
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.spanningSets.eq_1 : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ] (i : ℕ),
  MeasureTheory.spanningSets μ i = Set.accumulate μ.toFiniteSpanningSetsIn.set i
-- Lean.Message
Lean.MessageData.withContext.inj : ∀ {a : Lean.MessageDataContext} {a_1 : Lean.MessageData} {a_2 : Lean.MessageDataContext} {a_3 : Lean.MessageData},
  Lean.MessageData.withContext a a_1 = Lean.MessageData.withContext a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Topology.Order.IntermediateValue
denselyOrdered_of_preconnectedSpace : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [PreconnectedSpace α],
  DenselyOrdered α
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instInhabited : {G : Type u_1} → [inst : Group G] → Inhabited (Subgroup G)
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- If `B` is a cyclotomic extension of `A` given by roots of unity of order in `T` and `S ⊆ T`,
then `adjoin A { b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1 }` is a cyclotomic extension of `B`
given by roots of unity of order in `S`.  -/
IsCyclotomicExtension.union_left : ∀ (S T : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [h : IsCyclotomicExtension T A B],
  S ⊆ T → IsCyclotomicExtension S A ↥(Algebra.adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extInv_inv_hom : ∀ {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 c' : CategoryTheory.Limits.Cocone F} (φ : c.pt ≅ c'.pt)
  (w :
    autoParam (∀ (j : J), c.ι.app j = CategoryTheory.CategoryStruct.comp (c'.ι.app j) φ.inv)
      CategoryTheory.Limits.Cocone.extInv._auto_1),
  (CategoryTheory.Limits.Cocone.extInv φ w).inv.hom = φ.inv
-- Lean.LocalContext
Lean.instDecidableEqLocalDeclKind : DecidableEq Lean.LocalDeclKind
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The composition of right homology map data.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.comp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {φ' : S₂ ⟶ S₃} →
            {h₁ : S₁.RightHomologyData} →
              {h₂ : S₂.RightHomologyData} →
                {h₃ : S₃.RightHomologyData} →
                  CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂ →
                    CategoryTheory.ShortComplex.RightHomologyMapData φ' h₂ h₃ →
                      CategoryTheory.ShortComplex.RightHomologyMapData (CategoryTheory.CategoryStruct.comp φ φ') h₁ h₃
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapRingHom_comp : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Semiring T] [inst_3 : Monoid M] (f : S →+* T) (g : R →+* S),
  MonoidAlgebra.mapRingHom M (f.comp g) = (MonoidAlgebra.mapRingHom M f).comp (MonoidAlgebra.mapRingHom M g)
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.mappingConeHomOfDegreewiseSplitIso_hom_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting)
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (i : ℤ),
  (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).hom.f i =
    (CochainComplex.mappingConeHomOfDegreewiseSplitXIso S σ i (i + 1) ⋯).hom
-- Mathlib.Topology.Compactness.Compact
exists_nhds_ne_neBot : ∀ (X : Type u_2) [inst : TopologicalSpace X] [CompactSpace X] [Infinite X], ∃ z, (nhdsWithin z {z}ᶜ).NeBot
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nhdsWithin_Icc_isMeasurablyGenerated : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : Preorder α]
  {a b x : α} [OrderClosedTopology α], (nhdsWithin x (Set.Icc a b)).IsMeasurablyGenerated
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- A vector space over a field is isomorphic to its dual if and only if it is finite-dimensional:
a consequence of the Erdős-Kaplansky theorem.  -/
Basis.linearEquiv_dual_iff_finiteDimensional : ∀ {K : Type uK} {V : Type uV} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Nonempty (V ≃ₗ[K] Module.Dual K V) ↔ FiniteDimensional K V
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
/-- If the scalar multiplication `(· • ·) : α → β → β` is distributive,
then so is `(· • ·) : α → Finset β → Finset β`.  -/
Finset.distribSMul : {α : Type u_1} →
  {β : Type u_2} → [inst : DecidableEq β] → [inst_1 : AddZeroClass β] → [DistribSMul α β] → DistribSMul α (Finset β)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.surjOn_log : Set.SurjOn Real.log (Set.Ioi 0) Set.univ
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- Auxiliary definition for the proof of `Subsingleton (Φ.Iteration j)`.  -/
CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {K : Type w} →
      [inst_1 : LinearOrder K] →
        {x : K} →
          CategoryTheory.Functor (↑(Set.Iic x)) C →
            CategoryTheory.Functor (↑(Set.Iic x)) C → (k₁ k₂ : K) → k₁ ≤ k₂ → k₂ ≤ x → Prop
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roi.length_iter : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.Rxi.HasSize α] [Std.Rxi.LawfulHasSize α] {r : Std.Roi α},
  r.iter.length = r.size
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- `f.dualMap` is injective if and only if `f` is surjective  -/
LinearMap.dualMap_injective_iff : ∀ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V₁ →ₗ[K] V₂},
  Function.Injective ⇑f.dualMap ↔ Function.Surjective ⇑f
-- Mathlib.Tactic.GRewrite.Core
/-- The current progress level.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.State.progress : Mathlib.Tactic.GRewrite.State✝ → Mathlib.Tactic.GRewrite.Progress✝
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- **Alias** of `Finset.prod_eq_mul_prod_sdiff_singleton`. -/
Finset.prod_eq_mul_prod_diff_singleton : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} (i : ι) (f : ι → M),
  (i ∉ s → f i = 1) → ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.op_deg : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) (a : Cᵒᵖ), r.op.deg a = (r.deg ∘ Opposite.unop) a
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instInvolutiveNeg : {α : Type u_1} → [InvolutiveNeg α] → InvolutiveNeg αᵒᵈ
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Given two disjoint closed sets `s, t` in a Hausdorff σ-compact finite-dimensional manifold,
there exists an infinitely smooth function that is equal to `0` on `s` and to `1` on `t`.
See also `exists_contMDiff_zero_iff_one_iff_of_isClosed`, which ensures additionally that
`f` is equal to `0` exactly on `s` and to `1` exactly on `t`.  -/
exists_contMDiffMap_zero_one_of_isClosed : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] {n : ℕ∞} [T2Space M] [SigmaCompactSpace M] {s t : Set M},
  IsClosed s → IsClosed t → Disjoint s t → ∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Set.Icc 0 1
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_le_iff : ∀ {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s],
  Ordinal.type r ≤ Ordinal.type s ↔ Nonempty (InitialSeg r s)
-- Mathlib.Order.SetNotation
Set.mem_iInter : ∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, x ∈ ⋂ i, s i ↔ ∀ (i : ι), x ∈ s i
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint, if `B` is free and `A` is flat,
then `[A[B] : A] = [B : R]`. See also `Subalgebra.adjoin_rank_le`.  -/
Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_right : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ [Module.Free R ↥B] [Module.Flat R ↥A] [Nontrivial R] [Nontrivial S],
      Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B) = Module.rank R ↥B
-- Lean.Level
Lean.Level.PP.Result.brecOn.eq : ∀ {motive_1 : Lean.Level.PP.Result → Sort u} {motive_2 : List Lean.Level.PP.Result → Sort u} (t : Lean.Level.PP.Result)
  (F_1 : (t : Lean.Level.PP.Result) → t.below → motive_1 t)
  (F_2 : (t : List Lean.Level.PP.Result) → Lean.Level.PP.Result.below_1 t → motive_2 t),
  t.brecOn F_1 F_2 = F_1 t (Lean.Level.PP.Result.brecOn.go t F_1 F_2).2
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.setTag.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (cidx : ℕ)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_9) (fvarId_1 : Lean.FVarId)
  (cidx_1 : ℕ) (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_9),
  (Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h = Lean.Compiler.LCNF.CodeDecl.setTag fvarId_1 cidx_1 h_1) =
    (fvarId = fvarId_1 ∧ cidx = cidx_1)
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- Graded ring homomorphisms map zero to zero.  -/
GradedRingHom.map_zero : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ), f 0 = 0
-- Mathlib.Algebra.Regular.Basic
/-- In an additive semigroup, the sum of add-regular elements is add-regular.  -/
IsAddRegular.add : ∀ {R : Type u_1} [inst : AddSemigroup R] {a b : R}, IsAddRegular a → IsAddRegular b → IsAddRegular (a + b)
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.smulCommClass : ∀ (α : Type u_1) {G : Type u_3} [inst : Group G] [inst_1 : SMul α G] [SMulCommClass α G G] [IsScalarTower α G G],
  SMulCommClass α (ConjAct G) G
-- Mathlib.Topology.Algebra.Ring.Real
NNReal.instContinuousSMulOfReal : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MulAction ℝ α] [ContinuousSMul ℝ α], ContinuousSMul NNReal α
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
TensorProduct.fromDirectLimit_of_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Preorder ι]
  {G : ι → Type u_3} [inst_3 : (i : ι) → AddCommMonoid (G i)] [inst_4 : (i : ι) → Module R (G i)]
  (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) {M : Type u_4} [inst_5 : AddCommMonoid M] [inst_6 : Module R M] {i : ι}
  (g : G i) (m : M),
  (TensorProduct.fromDirectLimit f M)
      ((Module.DirectLimit.of R ι (fun x => TensorProduct R (G x) M) (fun i j h => LinearMap.rTensor M (f i j h)) i)
        (g ⊗ₜ[R] m)) =
    (Module.DirectLimit.of R ι G f i) g ⊗ₜ[R] m
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_ne_zero_of_isUnit_det : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R] [Nonempty n']
  [Nontrivial R] {A : Matrix n' n' R}, IsUnit A.det → ∀ (z : ℤ), A ^ z ≠ 0
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- **Alias** of `IsEllipticSequence`.

---

The proposition that a sequence indexed by `ℤ` is an elliptic sequence.  -/
IsEllSequence : {R : Type u_1} → [CommRing R] → (ℤ → R) → Prop
-- Mathlib.RingTheory.OreLocalization.Basic
/-- The addition on the Ore localization.  -/
_private.Mathlib.RingTheory.OreLocalization.Basic.0.OreLocalization.add : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} →
          [inst_2 : AddMonoid X] →
            [inst_3 : DistribMulAction R X] → OreLocalization S X → OreLocalization S X → OreLocalization S X
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
/-- The right inclusion in `Cocycle L (mappingCocone φ) 1`.  -/
CochainComplex.mappingCocone.inr : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (φ : K ⟶ L) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            CochainComplex.HomComplex.Cocycle L (CochainComplex.mappingCocone φ) 1
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.lt_add_lt : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [Lean.Grind.OrderedAdd α] {a b : α}, a < 0 → b < 0 → a + b < 0
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.star_exp : ∀ {𝔸 : Type u_2} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] [T2Space 𝔸]
  [inst_4 : StarRing 𝔸] [ContinuousStar 𝔸] (x : 𝔸), star (NormedSpace.exp x) = NormedSpace.exp (star x)
-- Lean.ScopedEnvExtension
Lean.SimpleScopedEnvExtension.Descr : Type → Type → Type
-- Lean.Meta.CongrTheorems
Lean.Meta.instReprCongrArgKind : Repr Lean.Meta.CongrArgKind
-- Mathlib.Order.Atoms
/-- A complemented modular atomic lattice is strongly coatomic.
Not an instance to prevent loops.  -/
ComplementedLattice.isStronglyAtomic' : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α] [ComplementedLattice α]
  [h : IsAtomic α], IsStronglyCoatomic α