mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.ε_comp_map_ε_assoc : ∀ {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} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.Monoidal] [adj.IsMonoidal] {Z : C}
  (h : G.obj (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε G)
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.LaxMonoidal.ε F)) h) =
    CategoryTheory.CategoryStruct.comp (adj.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffOn.vadd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {H'' : Type u_6} [inst_7 : TopologicalSpace H''] {E'' : Type u_7}
  [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E''] {I'' : ModelWithCorners 𝕜 E'' H''} {G : Type u_8}
  [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H G] {M : Type u_9} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace H'' N]
  [inst_16 : VAdd G M] {n : WithTop ℕ∞} [ContMDiffVAdd I I' n G M] {f : N → G} {g : N → M} {s : Set N},
  ContMDiffOn I'' I n f s → ContMDiffOn I'' I' n g s → ContMDiffOn I'' I' n (f +ᵥ g) s
-- Mathlib.RingTheory.Localization.Module
IsLocalizedModule.linearIndependent_lift : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_3} {Mₛ : Type u_4} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid Mₛ] [inst_4 : Module R Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f]
  {ι : Type u_5} {v : ι → Mₛ}, LinearIndependent R v → ∃ w, LinearIndependent R w
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- When lowered to a prop, `Matrix.invertibleEquivInvertibleFst` forms an `iff`.  -/
TrivSqZeroExt.isUnit_iff_isUnit_fst : ∀ {R : Type u} {M : Type v} [inst : AddCommGroup M] [inst_1 : Semiring R] [inst_2 : Module Rᵐᵒᵖ M] [inst_3 : Module R M]
  [inst_4 : SMulCommClass R Rᵐᵒᵖ M] {x : TrivSqZeroExt R M}, IsUnit x ↔ IsUnit x.fst
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.setMeta : Lean.ParseImports.Parser
-- Mathlib.Logic.Embedding.Basic
/-- An embedding, a.k.a. a bundled injective function.  -/
Function.«term_↪_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Star.StarAlgHom
/-- The first projection of a product is a ⋆-algebra homomorphism.  -/
StarAlgHom.fst : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Star A] → [inst_4 : Semiring B] → [inst_5 : Algebra R B] → [inst_6 : Star B] → A × B →⋆ₐ[R] A
-- Mathlib.Data.Multiset.AddSub
Multiset.sub_cons : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Multiset α), s - a ::ₘ t = s.erase a - t
-- Mathlib.CategoryTheory.Shift.SingleFunctorsLift
CategoryTheory.SingleFunctors.lift.shiftIso.eq_1 : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{u_5, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_6, u_2} D] [inst_2 : CategoryTheory.Category.{u_7, u_3} E] {A : Type u_4}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  {F : CategoryTheory.SingleFunctors C E A} {G : CategoryTheory.Functor D E} [inst_6 : G.CommShift A] [inst_7 : G.Full]
  [inst_8 : G.Faithful] {Φ : A → CategoryTheory.Functor C D} (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) (n a a' : A)
  (h : n + a = a'),
  CategoryTheory.SingleFunctors.lift.shiftIso hΦ n a a' h =
    ((CategoryTheory.Functor.FullyFaithful.ofFullyFaithful G).whiskeringRight C).preimageIso
      ((Φ a').associator (CategoryTheory.shiftFunctor D n) G ≪≫
        (Φ a').isoWhiskerLeft (CategoryTheory.Functor.commShiftIso G n) ≪≫
          ((Φ a').associator G (CategoryTheory.shiftFunctor E n)).symm ≪≫
            CategoryTheory.Functor.isoWhiskerRight (hΦ a') (CategoryTheory.shiftFunctor E n) ≪≫
              F.shiftIso n a a' h ≪≫ (hΦ a).symm)
-- Mathlib.Algebra.Order.Module.Field
inv_smul_le_iff_of_neg : ∀ {𝕜 : Type u_1} {G : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup G] [inst_4 : PartialOrder G] [IsOrderedAddMonoid G] [inst_6 : Module 𝕜 G] {a : 𝕜} {b₁ b₂ : G}
  [PosSMulMono 𝕜 G], a < 0 → (a⁻¹ • b₁ ≤ b₂ ↔ a • b₂ ≤ b₁)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_inv_of_apply_inv_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : InvolutiveInv α] {s : Set α} {f g : α → β},
  (∀ x ∈ s, f x⁻¹ = g x) → f '' s⁻¹ = g '' s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval_shiftLeft : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {a : ℕ} {lhs : Std.Tactic.BVDecide.BVExpr a} {a_1 : ℕ}
  {rhs : Std.Tactic.BVDecide.BVExpr a_1},
  Std.Tactic.BVDecide.BVExpr.eval assign (lhs.shiftLeft rhs) =
    Std.Tactic.BVDecide.BVExpr.eval assign lhs <<< Std.Tactic.BVDecide.BVExpr.eval assign rhs
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.ae_le_of_forall_setIntegral_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ →
      (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ) → f ≤ᵐ[μ] g
-- Mathlib.LinearAlgebra.BilinearMap
/-- A version of `Function.Surjective.comp` for composition of a bilinear map with a linear map.  -/
LinearMap.surjective_compr₂ₛₗ_of_equiv : ∀ {R : Type u_2} [inst : CommSemiring R] {R₂ : Type u_14} {R₃ : Type u_15} {R₄ : Type u_16} {M : Type u_17}
  {N : Type u_18} {P : Type u_19} {Q : Type u_20} [inst_1 : CommSemiring R₂] [inst_2 : CommSemiring R₃]
  [inst_3 : CommSemiring R₄] [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P]
  [inst_7 : AddCommMonoid Q] [inst_8 : Module R M] [inst_9 : Module R₂ N] [inst_10 : Module R₃ P]
  [inst_11 : Module R₄ Q] {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄}
  {σ₄₃ : R₄ →+* R₃} [inst_12 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [inst_15 : RingHomInvPair σ₃₄ σ₄₃] [inst_16 : RingHomInvPair σ₄₃ σ₃₄]
  (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (g : P ≃ₛₗ[σ₃₄] Q), Function.Surjective ⇑f → Function.Surjective ⇑(f.compr₂ₛₗ ↑g)
-- Mathlib.Data.LawfulXor.Basic
instLawfulXorUInt32 : LawfulXor UInt32
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.toFinsuppIsoAlg_apply : ∀ (R : Type u) [inst : CommSemiring R] (self : Polynomial R), (Polynomial.toFinsuppIsoAlg R) self = self.toFinsupp
-- Mathlib.Topology.Bases
TopologicalSpace.isSeparable_range : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [inst : TopologicalSpace β] [TopologicalSpace.SeparableSpace α]
  {f : α → β}, Continuous f → TopologicalSpace.IsSeparable (Set.range f)
-- Mathlib.CategoryTheory.FintypeCat
/-- The category of finite types.  -/
FintypeCat : Type (u_1 + 1)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- A continuous surjective additive monoid homomorphism of topological groups with compact
codomain is measure preserving, provided that the Haar measures on the domain and on the codomain
have the same total mass.  -/
AddMonoidHom.measurePreserving : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] {H : Type u_2} [inst_5 : AddGroup H] [inst_6 : TopologicalSpace H]
  [IsTopologicalAddGroup H] [CompactSpace H] [inst_9 : MeasurableSpace H] [BorelSpace H] {μ : MeasureTheory.Measure G}
  [μ.IsAddHaarMeasure] {ν : MeasureTheory.Measure H} [ν.IsAddHaarMeasure] {f : G →+ H},
  Continuous ⇑f → Function.Surjective ⇑f → μ Set.univ = ν Set.univ → MeasureTheory.MeasurePreserving (⇑f) μ ν
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- See Note [custom simps projection].
We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
ContinuousAffineEquiv.Simps.apply : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : Module k V₁] →
                [inst_3 : AddTorsor V₁ P₁] →
                  [inst_4 : TopologicalSpace P₁] →
                    [inst_5 : AddCommGroup V₂] →
                      [inst_6 : Module k V₂] →
                        [inst_7 : AddTorsor V₂ P₂] → [inst_8 : TopologicalSpace P₂] → (P₁ ≃ᴬ[k] P₂) → P₁ → P₂
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- The existence of binary biproducts implies that there is at most one preadditive structure.  -/
CategoryTheory.Limits.biprod.add_eq_lift_desc_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} (f g : X ⟶ Y)
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct Y Y],
  f + g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g)
      (CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y))
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuous_sub_right : ∀ (a : ENNReal), Continuous fun x => x - a
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The uniqueness of `lift`.  -/
CategoryTheory.WithTerminal.liftUnique : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {Z : D} →
          (F : CategoryTheory.Functor C D) →
            (M : (x : C) → F.obj x ⟶ Z) →
              (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) →
                (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) →
                  (h : CategoryTheory.WithTerminal.incl.comp G ≅ F) →
                    (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) →
                      (∀ (x : C),
                          CategoryTheory.CategoryStruct.comp
                              (G.map
                                (CategoryTheory.WithTerminal.starTerminal.from
                                  (CategoryTheory.WithTerminal.incl.obj x)))
                              hG.hom =
                            CategoryTheory.CategoryStruct.comp (h.hom.app x) (M x)) →
                        (G ≅ CategoryTheory.WithTerminal.lift F M hM)
-- Mathlib.Algebra.Category.MonCat.Yoneda
CommMonCat.coyonedaType_obj_obj_coe : ∀ (X : Type uᵒᵖ) (M : CommMonCat), ↑((CommMonCat.coyonedaType.obj X).obj M) = (Opposite.unop X → ↑M)
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff_source : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (M : Type w')
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] {X : C} [W.IsCompatibleWithShift M] {X' : C}
  (f : X ⟶ X'),
  W f →
    ∀ (Y : C),
      CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y ↔
        CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X' Y
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.uSwitchEquiv.eq_1 : ∀ (X : FintypeCat), X.uSwitchEquiv = Equiv.ulift.trans (Fintype.equivFin X.obj).symm
-- Mathlib.Algebra.Star.Pointwise
Set.star_singleton : ∀ {β : Type u_2} [inst : InvolutiveStar β] (x : β), star {x} = {star x}
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Construct an algebra isomorphism from an equality of intermediate fields.  -/
IntermediateField.equivOfEq : {F : Type u_4} →
  [inst : Field F] →
    {E : Type u_5} → [inst_1 : Field E] → [inst_2 : Algebra F E] → {S T : IntermediateField F E} → S = T → ↥S ≃ₐ[F] ↥T
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_eq_iff_eq_mul_left : ∀ {a b c : ℤ}, b ≠ 0 → b ∣ a → (a.tdiv b = c ↔ a = c * b)
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_neg : ∀ {R : Type u_10} {R₂ : Type u_11} {M : Type u_12} {M₂ : Type u_13} [inst : Semiring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂), (-f).range = f.range
-- Mathlib.Analysis.Normed.Module.Ball.Action
mulActionSphereClosedBall : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [NormedSpace 𝕜 E] → {r : ℝ} → MulAction ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)
-- Mathlib.Algebra.Module.LinearMap.Defs
SemilinearMapClass.toAddHomClass : ∀ {F : Type u_14} {R : outParam (Type u_15)} {S : outParam (Type u_16)} {inst : Semiring R} {inst_1 : Semiring S}
  {σ : outParam (R →+* S)} {M : outParam (Type u_17)} {M₂ : outParam (Type u_18)} {inst_2 : AddCommMonoid M}
  {inst_3 : AddCommMonoid M₂} {inst_4 : Module R M} {inst_5 : Module S M₂} {inst_6 : FunLike F M M₂}
  [self : SemilinearMapClass F σ M M₂], AddHomClass F M M₂
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.TranslateData.mk : Lean.NameMapExtension (List ℕ) →
  Lean.NameMapExtension Bool →
    Option Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt →
      Lean.NameMapExtension Mathlib.Tactic.Translate.TranslationInfo →
        Lean.Name → Bool → Bool → Mathlib.Tactic.GuessName.GuessNameExt → Mathlib.Tactic.Translate.TranslateData
-- Lean.Environment
/-- Reverse list of ongoing `realizeConst` calls, used to restrict env ext modifications and detect
cyclic realizations.
 -/
_private.Lean.Environment.0.Lean.AsyncContext.realizingStack : Lean.AsyncContext✝ → List Lean.Name
-- Mathlib.Probability.Process.Stopping
MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {μ : MeasureTheory.Measure Ω}
  {ℱ : MeasureTheory.Filtration ι m} {τ : Ω → WithTop ι} {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [CompleteSpace E] {f : Ω → E} [Countable ι] [MeasureTheory.SigmaFiniteFiltration μ ℱ]
  (hτ : MeasureTheory.IsStoppingTime ℱ τ) [MeasureTheory.SigmaFinite (μ.trim ⋯)] (i : ι),
  μ[f | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = ↑i}] μ[f | ↑ℱ i]
-- Mathlib.NumberTheory.TsumDivisorsAntidiagonal
sigmaAntidiagonalEquivProd_symm_apply_fst : ∀ (x : ℕ+ × ℕ+), ↑(sigmaAntidiagonalEquivProd.symm x).fst = ↑x.1 * ↑x.2
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The inverse of a continuous linear equivalence as a continuous linear equivalence  -/
ContinuousLinearEquiv.symm : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {σ₂₁ : R₂ →+* R₁} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                {M₁ : Type u_4} →
                  [inst_4 : TopologicalSpace M₁] →
                    [inst_5 : AddCommMonoid M₁] →
                      {M₂ : Type u_5} →
                        [inst_6 : TopologicalSpace M₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R₁ M₁] → [inst_9 : Module R₂ M₂] → (M₁ ≃SL[σ₁₂] M₂) → M₂ ≃SL[σ₂₁] M₁
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_diff_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ \ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∈ t₂
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.Uniformizer.ne_zero : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] {v : Valuation A Γ}
  [hv : v.IsRankOneDiscrete] (π : v.Uniformizer), ↑π.val ≠ 0
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max_erase_eq_iff_not_compare_eq_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, (t.erase k).max he = t.max ⋯ ↔ ¬cmp k (t.max ⋯) = Ordering.eq
-- Mathlib.Tactic.FunProp.Types
/-- Name to unfold  -/
Mathlib.Meta.FunProp.Context.constToUnfold : Mathlib.Meta.FunProp.Context → Std.TreeSet Lean.Name Lean.Name.quickCmp
-- Lean.Compiler.Specialize
/-- Marks a definition to never be specialized during code generation.
 -/
Lean.Compiler.nospecializeAttr : Lean.TagAttribute
-- Init.Data.Slice.List.Basic
/-- Internal representation of `ListSlice`, which is an abbreviation for `Slice ListSliceData`.
 -/
Std.Slice.Internal.ListSliceData : Type u → Type u
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₃ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).inv.app X).hom₃ =
    (CategoryTheory.shiftFunctorZero C ℤ).inv.app X.obj₃
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.adjoint_lTensor : ∀ {𝕜 : Type u_1} (E : Type u_2) {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 G]
  [inst_5 : NormedAddCommGroup H] [inst_6 : InnerProductSpace 𝕜 H] [CompleteSpace E] [inst_8 : CompleteSpace G]
  [inst_9 : CompleteSpace (TensorProduct 𝕜 E H)] [inst_10 : CompleteSpace (TensorProduct 𝕜 E G)]
  [inst_11 : CompleteSpace H] (g : G →L[𝕜] H),
  ContinuousLinearMap.adjoint (ContinuousLinearMap.lTensor E g) =
    ContinuousLinearMap.lTensor E (ContinuousLinearMap.adjoint g)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.le_rpow_inv_iff_of_neg : ∀ {x : NNReal} {z : ℝ} {y : NNReal}, 0 < x → 0 < y → z < 0 → (x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBasis.isBasis_of_closure_eq_closure : ∀ {α : Type u_2} {M : Matroid α} {X Y I : Set α},
  M.IsBasis I X →
    I ⊆ Y →
      M.closure X = M.closure Y →
        autoParam (Y ⊆ M.E) Matroid.IsBasis.isBasis_of_closure_eq_closure._auto_1 → M.IsBasis I Y
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `lt_of_mul_lt_mul_left`. -/
lt_of_mul_lt_mul_of_nonneg_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [PosMulReflectLT α],
  a * b < a * c → 0 ≤ a → b < c
-- Std.Time.Time.PlainTime
/-- `Minute` component of the `PlainTime`
 -/
Std.Time.PlainTime.minute : Std.Time.PlainTime → Std.Time.Minute.Ordinal
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.ofHom_comp : ∀ {R : Type u} [inst : CommRing R] {X Y Z : Type v} [inst_1 : CommRing X] [inst_2 : HopfAlgebra R X]
  [inst_3 : CommRing Y] [inst_4 : HopfAlgebra R Y] [inst_5 : CommRing Z] [inst_6 : HopfAlgebra R Z] (f : X →ₐc[R] Y)
  (g : Y →ₐc[R] Z),
  CommHopfAlgCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.ofHom f) (CommHopfAlgCat.ofHom g)
-- Qq.MatchImpl
Lean.Syntax.stripPos : Lean.Syntax → Lean.Syntax
-- Mathlib.RingTheory.WittVector.StructurePolynomial
constantCoeff_wittStructureInt : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ),
  MvPolynomial.constantCoeff Φ = 0 → ∀ (n : ℕ), MvPolynomial.constantCoeff (wittStructureInt p Φ n) = 0
-- Init.Grind.Util
Lean.Grind.offsetUnexpander : Lean.PrettyPrinter.Unexpander
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_insertMany_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {ρ : Type v} [inst : ForIn Id ρ α] [EquivBEq α]
  [LawfulHashable α] {l : ρ} {k : α}, k ∈ m → k ∈ m.insertMany l
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategoryᵒᵖ}
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ'),
  CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ).inj A)
      ((AlgebraicTopology.DoldKan.Γ₀.obj K).map θ) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K
        (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e)))
      (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ').inj (A.pull θ))
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ`. -/
Topology.CWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ),
  ↑(Topology.RelCWComplex.skeletonLT C ↑n) ∪ ⋃ j, Topology.RelCWComplex.closedCell n j =
    ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1))
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.isUnit_C_add_X_mul_iff : ∀ {R : Type u_1} {r : R} [inst : CommRing R] {P : Polynomial R},
  IsUnit (Polynomial.C r + Polynomial.X * P) ↔ IsUnit r ∧ IsNilpotent P
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
/-- The domain of the adjoint operator.

This definition is needed to construct the adjoint operator and the preferred version to use is
`T.adjoint.domain` instead of `T.adjointDomain`.  -/
LinearPMap.adjointDomain : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : InnerProductSpace 𝕜 F] → (E →ₗ.[𝕜] F) → Submodule 𝕜 F
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.mk_ne_zero_of_degree_lt : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R},
  f.Monic → ∀ {g : Polynomial R}, g ≠ 0 → g.degree < f.degree → (AdjoinRoot.mk f) g ≠ 0
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.isEdgeReachable_add_one : ∀ {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {u v : V},
  k ≠ 0 → (G.IsEdgeReachable (k + 1) u v ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v)
-- Mathlib.LinearAlgebra.Basis.MulOpposite
MulOpposite.instFree : ∀ {R : Type u_1} {H : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid H] [inst_2 : Module R H] [Module.Free R H],
  Module.Free R Hᵐᵒᵖ
-- Mathlib.Algebra.Module.ZLattice.Basic
Module.Basis.ofZLatticeBasis_span : ∀ (K : Type u_1) [inst : NormedField K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  [inst_3 : HasSolidNorm K] [inst_4 : FloorRing K] {E : Type u_2} [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace K E] [inst_7 : FiniteDimensional K E] [inst_8 : ProperSpace E] (L : Submodule ℤ E)
  [inst_9 : DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L] (b : Module.Basis ι ℤ ↥L),
  Submodule.span ℤ (Set.range ⇑(Module.Basis.ofZLatticeBasis K L b)) = L
-- Mathlib.Algebra.GroupWithZero.Associated
IsRelPrime.eq_1 : ∀ {α : Type u_1} [inst : Monoid α] (x y : α), IsRelPrime x y = ∀ ⦃d : α⦄, d ∣ x → d ∣ y → IsUnit d
-- Mathlib.Data.Tree.Basic
BinaryTree.traverse.eq_2 : ∀ {m : Type u_1 → Type u_2} [inst : Applicative m] {α : Type u_3} {β : Type u_1} (f : α → m β) (a : α)
  (l r : BinaryTree α),
  BinaryTree.traverse f (BinaryTree.node a l r) =
    BinaryTree.node <$> f a <*> BinaryTree.traverse f l <*> BinaryTree.traverse f r
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.IterM.Equiv.toIter : ∀ {α₁ α₂ β : Type u_1} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] {ita : Std.IterM Id β}
  {itb : Std.IterM Id β}, ita.Equiv itb → ita.toIter.Equiv itb.toIter
-- Mathlib.Analysis.Convex.LinearIsometry
LinearIsometryEquiv.strictConvexSpace_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F]
  (e : E ≃ₗᵢ[𝕜] F), StrictConvexSpace 𝕜 E ↔ StrictConvexSpace 𝕜 F