mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TensorProduct.Quotient
Algebra.tensorQuotientTensorEquiv.eq_1 : ∀ {R : Type u_1} {R' : Type u_2} (R'' : Type u_3) {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing R']
  [inst_2 : CommRing R''] [inst_3 : CommRing S] [inst_4 : Algebra R R'] [inst_5 : Algebra R R'']
  [inst_6 : Algebra R' R''] [inst_7 : IsScalarTower R R' R''] [inst_8 : Algebra R S] (e : TensorProduct R R' S),
  Algebra.tensorQuotientTensorEquiv R'' e =
    AlgEquiv.ofAlgHom
      (Algebra.TensorProduct.lift
        (Algebra.ofId R''
          (TensorProduct R R'' S ⧸ Ideal.span {(Algebra.TensorProduct.rTensor S (Algebra.ofId R' R'')) e}))
        (Ideal.quotientMapₐ (Ideal.span {(Algebra.TensorProduct.rTensor S (Algebra.ofId R' R'')) e})
          (Algebra.TensorProduct.rTensor S (Algebra.ofId R' R'')) ⋯)
        ⋯)
      (Ideal.Quotient.liftₐ (Ideal.span {(Algebra.TensorProduct.rTensor S (Algebra.ofId R' R'')) e})
        (Algebra.TensorProduct.lift (Algebra.ofId R'' (TensorProduct R' R'' (TensorProduct R R' S ⧸ Ideal.span {e})))
          ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp
            ((Ideal.Quotient.mkₐ R (Ideal.span {e})).comp Algebra.TensorProduct.includeRight))
          ⋯)
        ⋯)
      ⋯ ⋯
-- Init.Data.List.Lemmas
List.head?_eq_getLast?_reverse : ∀ {α : Type u_1} {xs : List α}, xs.head? = xs.reverse.getLast?
-- Mathlib.Geometry.Convex.Cone.TensorProduct
PointedCone.map.eq_1 : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] [inst_5 : AddCommMonoid F] [inst_6 : Module R F] (f : E →ₗ[R] F)
  (C : PointedCone R E), PointedCone.map f C = Submodule.map (↑{ c // 0 ≤ c } f) C
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- If `F ⋙ G` preserves finite limits and `G` reflects finite limits, then `F` preserves
finite limits.
 -/
CategoryTheory.Limits.preservesFiniteLimits_of_reflects_of_preserves : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteLimits (F.comp G)]
  [CategoryTheory.Limits.ReflectsFiniteLimits G], CategoryTheory.Limits.PreservesFiniteLimits F
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_ord_le : ∀ (c : Cardinal.{u_1}), c.ord.cof ≤ c
-- Mathlib.Data.EReal.Inv
_private.Mathlib.Data.EReal.Inv.0.EReal.exists_lt_mul_left_of_nonneg : ∀ {a b c : EReal}, 0 ≤ a → 0 ≤ c → c < a * b → ∃ a' ∈ Set.Ioo 0 a, c < a' * b
-- Mathlib.RingTheory.Ideal.Pure
/-- [Stacks Tag 04PS](https://stacks.math.columbia.edu/tag/04PS) ((1) => (5)) -/
Ideal.exists_eq_mul_of_pure : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} [I.Pure] {x : R}, x ∈ I → ∃ y ∈ I, x = x * y
-- Mathlib.RepresentationTheory.Rep.Res
/-- Morphism between `X Y : Rep k G` can be lifted from restrictions associated with `f : H →* G`
when `f` is surjective.  -/
Rep.liftHomOfSurj : {k : Type u} →
  [inst : Semiring k] →
    {G : Type v1} →
      {H : Type v2} →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] →
            (f : H →* G) → {X Y : Rep.{u_1, u, v1} k G} → Function.Surjective ⇑f → (Rep.res f X ⟶ Rep.res f Y) → (X ⟶ Y)
-- Mathlib.GroupTheory.Congruence.Defs
AddConGen.Rel.below : {M : Type u_1} →
  [inst : Add M] →
    {r : M → M → Prop} →
      {motive : (a a_1 : M) → AddConGen.Rel r a a_1 → Prop} → {a a_1 : M} → AddConGen.Rel r a a_1 → Prop
-- Mathlib.Order.Filter.Basic
Filter.iInf_neBot_iff_of_directed : ∀ {α : Type u} {ι : Sort x} {f : ι → Filter α} [Nonempty α],
  Directed (fun x1 x2 => x1 ≥ x2) f → ((iInf f).NeBot ↔ ∀ (i : ι), (f i).NeBot)
-- Mathlib.SetTheory.Ordinal.Veblen
_private.Mathlib.SetTheory.Ordinal.Veblen.0.Ordinal.cmp_veblenWith.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.eq) (h_2 : Unit → motive Ordering.lt)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.gt with
    | Ordering.eq => h_1 ()
    | Ordering.lt => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_3 ()
-- Init.Data.SInt.Bitwise
Int16.or_comm : ∀ (a b : Int16), a ||| b = b ||| a
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotient_map_comp_mkₐ : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Ring B] [inst_4 : Algebra R₁ B] {I : Ideal A} (J : Ideal B) [inst_5 : I.IsTwoSided] [inst_6 : J.IsTwoSided]
  (f : A →ₐ[R₁] B) (H : I ≤ Ideal.comap f J),
  (Ideal.quotientMapₐ J f H).comp (Ideal.Quotient.mkₐ R₁ I) = (Ideal.Quotient.mkₐ R₁ J).comp f
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- A version of `measurable_div_const` that assumes `MeasurableMul` instead of
`MeasurableDiv`. This can be nice to avoid unnecessary type-class assumptions.  -/
measurable_div_const' : ∀ {G : Type u_2} [inst : DivInvMonoid G] [inst_1 : MeasurableSpace G] [MeasurableMul G] (g : G),
  Measurable fun h => h / g
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanQueryModuleResponse.toJson : Lean.Lsp.LeanQueryModuleResponse → Lean.Json
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.multiplicativeClosure_morphismPropertyHomMk : ∀ {V : SSet.Truncated 2}, (SSet.Truncated.HomotopyCategory.morphismPropertyHomMk V).multiplicativeClosure = ⊤
-- Mathlib.AlgebraicGeometry.Artinian
/-- See `isLocallyArtinian_of_isImmersion`.  -/
_private.Mathlib.AlgebraicGeometry.Artinian.0.AlgebraicGeometry.IsLocallyArtinian.of_isOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f]
  [AlgebraicGeometry.IsLocallyArtinian Y], AlgebraicGeometry.IsLocallyArtinian X
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.Hom.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} →
      {c c' : C} →
        {S₁ S₂ : CategoryTheory.Span Wₗ Wᵣ c c'} →
          (hom : S₁.apex ⟶ S₂.apex) →
            autoParam (CategoryTheory.CategoryStruct.comp hom S₂.l = S₁.l) CategoryTheory.Span.Hom.hom_l._autoParam →
              autoParam (CategoryTheory.CategoryStruct.comp hom S₂.r = S₁.r) CategoryTheory.Span.Hom.hom_r._autoParam →
                S₁.Hom S₂
-- Mathlib.Data.Set.Prod
Set.univ_pi_nonempty_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)}, (Set.univ.pi t).Nonempty ↔ ∀ (i : ι), (t i).Nonempty
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
ChainComplex.isIso_descOpcycles_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : ChainComplex C ℕ) {X : C} (φ : K.X 0 ⟶ X) [inst_2 : HomologicalComplex.HasHomology K 0]
  (hφ : CategoryTheory.CategoryStruct.comp (K.d 1 0) φ = 0),
  CategoryTheory.IsIso (HomologicalComplex.descOpcycles K φ 1 ChainComplex.isIso_descOpcycles_iff._proof_1 hφ) ↔
    { X₁ := K.X 1, X₂ := K.X 0, X₃ := X, f := K.d 1 0, g := φ, zero := hφ }.Exact ∧ CategoryTheory.Epi φ
-- Init.Data.UInt.Lemmas
USize.sub_le : ∀ {a b : USize}, b ≤ a → a - b ≤ a
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.forgetToTop_of : ∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : AlexandrovDiscrete α],
  (CategoryTheory.forget₂ AlexDisc TopCat).obj (AlexDisc.of α) = TopCat.of α
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.hom_comp : ∀ {M N O : SemiNormedGrp} (f : M ⟶ N) (g : N ⟶ O),
  SemiNormedGrp.Hom.hom (CategoryTheory.CategoryStruct.comp f g) =
    (SemiNormedGrp.Hom.hom g).comp (SemiNormedGrp.Hom.hom f)
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy integral formula for the first order derivative**, assuming `f` is continuous on a
closed ball and differentiable on its interior away from a countable set.  -/
Complex.differentiable_on_off_countable_deriv_eq_smul_circleIntegral : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {f : ℂ → E} {c : ℂ}
  {s : Set ℂ},
  0 < R →
    s.Countable →
      ContinuousOn f (Metric.closedBall c R) →
        (∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z) →
          ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ 2) • f z = (2 * ↑Real.pi * Complex.I) • deriv f c
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.ext_iff : ∀ {α : Type u} [inst : AddMonoid α] {u v : AddUnits α}, u = v ↔ ↑u = ↑v
-- Batteries.Recycling.RBTree.WF
/-- If `t` has the red-red invariant, then setting the root to black yields a balanced tree.  -/
RBTree.RBNode.RedRed.setBlack : ∀ {α : Type u_1} {t : RBTree.RBNode α} {p : Prop} {n : ℕ},
  RBTree.RBNode.RedRed p t n → ∃ n', t.setBlack.Balanced RBTree.RBColor.black n'
-- Mathlib.FieldTheory.PurelyInseparable.Basic
Field.finInsepDegree.eq_1 : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Field.finInsepDegree F E = Module.finrank (↥(separableClosure F E)) E
-- Mathlib.Algebra.Order.Group.Defs
/-- **Alias** of `le_of_add_le_add_left`. -/
OrderedCommGroup.le_of_add_le_add_left : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α] [AddLeftReflectLE α] {a b c : α}, a + b ≤ a + c → b ≤ c
-- Batteries.Data.List.Lemmas
List.disjoint_cons_left : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Disjoint l₂ ↔ a ∉ l₂ ∧ l₁.Disjoint l₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
ClosedEmbeddingContinuousFunctionalCalculus.mk : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A]
  [inst_6 : StarRing A] [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A]
  [toContinuousFunctionalCalculus : ContinuousFunctionalCalculus R A p],
  (∀ (a : A) (ha : p a), Topology.IsClosedEmbedding ⇑(cfcHom ha)) → ClosedEmbeddingContinuousFunctionalCalculus R A p
-- Mathlib.CategoryTheory.Preadditive.FunctorCategory
CategoryTheory.NatTrans.app_nsmul : ∀ {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.Preadditive D]
  {F G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G) (n : ℕ), (n • α).app X = n • α.app X
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
instLieGroupOfTopWithTopENat : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] {a : WithTop ℕ∞} [LieGroup I ⊤ G],
  LieGroup I a G
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.mk.sizeOf_spec : ∀ {α₁ : Type w} {m : Type w → Type w'} {β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : SizeOf α₁]
  [inst_2 : (a : Type w) → SizeOf (m a)] [inst_3 : SizeOf β₁] [inst_4 : SizeOf α₂] [inst_5 : SizeOf β₂]
  (left : Std.IterM m β₁) (memoizedLeft : Option { out // ∃ it, it.IsPlausibleOutput out }) (right : Std.IterM m β₂),
  sizeOf { left := left, memoizedLeft := memoizedLeft, right := right } =
    1 + sizeOf left + sizeOf memoizedLeft + sizeOf right
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.precompEquiv_symm_apply : ∀ {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 Y Z : C} [inst_3 : W.RespectsIso]
  [inst_4 : W.IsCompatibleWithShift M] [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X X]
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y X]
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z]
  [inst_10 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z]
  [inst_11 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z] (f : X ⟶ Y) (hf : W f) {a : M}
  (β : CategoryTheory.Localization.SmallShiftedHom W X Z a),
  (CategoryTheory.Localization.SmallShiftedHom.precompEquiv f hf).symm β =
    (CategoryTheory.Localization.SmallShiftedHom.mk₀Inv 0 ⋯ f hf).comp β ⋯
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- If `f : ι → G × G` converges to the uniformity, then any `g : ι → G × G`
converges to the uniformity iff `f + g` does. This is often useful when `f` is valued in the
diagonal, in which case its convergence is automatic.  -/
Filter.Tendsto.uniformity_add_iff_right : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {f g : ι → α × α}
  {l : Filter ι},
  Filter.Tendsto f l (uniformity α) → (Filter.Tendsto (f + g) l (uniformity α) ↔ Filter.Tendsto g l (uniformity α))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSemanticTokensParams.fromJson : Lean.Json → Except String Lean.Lsp.SemanticTokensParams
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
Homeomorph.toOpenPartialHomeomorph_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y),
  e.toOpenPartialHomeomorph.source = Set.univ
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
/-- **Alias** of `CategoryTheory.SimplicialObject.Homotopy.sSetChainComplexMap`.

---

If `f` and `g` are simplicially homotopic maps of simplicial sets,
then they induce chain-homotopic maps on the singular chain complexes
with coefficients in `R`. The assumption is in `SimplicialObject.Homotopy`,
see also `SSet.Homotopy.chainComplexMap` for the
variant using `SSet.Homotopy` as an assumption.
 -/
CategoryTheory.SimplicialObject.Homotopy.singularChainComplexFunctorObjMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasCoproducts C] →
        {X Y : SSet} →
          {f g : X ⟶ Y} →
            CategoryTheory.SimplicialObject.Homotopy f g →
              (R : C) → Homotopy (SSet.chainComplexMap f R) (SSet.chainComplexMap g R)
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.directSum.eq_1 : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_1) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₁ : Type v₁}
  {ι₂ : Type v₂} [inst_3 : DecidableEq ι₁] [inst_4 : DecidableEq ι₂] (M₁ : ι₁ → Type w₁) (M₂ : ι₂ → Type w₂)
  [inst_5 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [inst_6 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)]
  [inst_7 : (i₁ : ι₁) → Module R (M₁ i₁)] [inst_8 : (i₂ : ι₂) → Module R (M₂ i₂)]
  [inst_9 : (i₁ : ι₁) → Module S (M₁ i₁)] [inst_10 : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)],
  TensorProduct.directSum R S M₁ M₂ =
    LinearEquiv.ofLinearMap
      (TensorProduct.AlgebraTensorModule.lift
        (DirectSum.toModule S ι₁
          ((DirectSum ι₂ fun i₂ => M₂ i₂) →ₗ[R] DirectSum (ι₁ × ι₂) fun i => TensorProduct R (M₁ i.1) (M₂ i.2))
          fun i₁ =>
          (DirectSum.toModule R ι₂ (M₁ i₁ →ₗ[S] DirectSum (ι₁ × ι₂) fun i => TensorProduct R (M₁ i.1) (M₂ i.2))
              fun i₂ =>
              (TensorProduct.AlgebraTensorModule.curry
                  (DirectSum.lof S (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂))).flip).flip))
      (DirectSum.toModule S (ι₁ × ι₂) (TensorProduct R (DirectSum ι₁ fun i₁ => M₁ i₁) (DirectSum ι₂ fun i₂ => M₂ i₂))
        fun i => TensorProduct.AlgebraTensorModule.map (DirectSum.lof S ι₁ M₁ i.1) (DirectSum.lof R ι₂ M₂ i.2))
      ⋯ ⋯
-- Init.Data.BitVec.Lemmas
/-- A bitvector, when interpreted as an integer, is less than zero iff
its most significant bit is true.
 -/
BitVec.slt_zero_iff_msb_cond : ∀ {w : ℕ} {x : BitVec w}, x.slt 0#w = true ↔ x.msb = true
-- Mathlib.Algebra.GroupWithZero.Regular
/-- In a non-trivial ring, the element `0` is not regular -- with typeclasses.  -/
not_isRegular_zero : ∀ {R : Type u_1} [inst : MulZeroClass R] [Nontrivial R], ¬IsRegular 0
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
CategoryTheory.IsNormalEpiCategory.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f], Nonempty (CategoryTheory.NormalEpi f)) →
    CategoryTheory.IsNormalEpiCategory C
-- Mathlib.Algebra.Order.Group.MinMax
min_div_div_left' : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] (a b c : α),
  min (a / b) (a / c) = a / max b c
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprMVarId_mathlib.toExpr : Lean.MVarId → Lean.Expr
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.sum_zero : ∀ {α : Type u_1} {n : ℤ} {f : α → ℤ} {s : Finset α}, (∀ x ∈ s, f x ≡ 0 [ZMOD n]) → ∑ x ∈ s, f x ≡ 0 [ZMOD n]
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.pullback_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (x : CategoryTheory.Subobject X), (CategoryTheory.Subobject.pullback (CategoryTheory.CategoryStruct.id X)).obj x = x
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.restrictPreimage_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty)
  (z : ↑(proj ⁻¹' s)), ↑(e.restrictPreimage hs) z = (⟨proj ↑z, ⋯⟩, (↑e.toPretrivialization ↑z).2)
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.fixed_eq_iInter_fixedBy : ∀ (M : Type u_1) (α : Type u_3) [inst : Monoid M] [inst_1 : MulAction M α],
  MulAction.fixedPoints M α = ⋂ m, MulAction.fixedBy α m
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.le_filtration : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι) (i : ι),
  A ≤ f.filtration i
-- Mathlib.Analysis.Complex.Trigonometric
Real.sinh_add : ∀ (x y : ℝ), Real.sinh (x + y) = Real.sinh x * Real.cosh y + Real.cosh x * Real.sinh y
-- Mathlib.Data.Set.Function
Set.InjOn.bijOn_image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s → Set.BijOn f s (f '' s)
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mk_eq_iff : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Invertible R M] {N : CommRing.Pic R}, CommRing.Pic.mk R M = N ↔ Nonempty (M ≃ₗ[R] N.AsModule)
-- Init.Data.Option.Attach
Option.attachWith_map : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} (f : α → β) {P : β → Prop}
  {H : ∀ (b : β), Option.map f o = some b → P b},
  (Option.map f o).attachWith P H =
    Option.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, h⟩)
      (o.attachWith (P ∘ f) ⋯)
-- Lean.Meta.Sym.AlphaShareBuilder
/-- `mkAppRevRangeS f b e revArgs` ==> `mkAppRev f (revArgs.extract b e)` with max sharing.  -/
Lean.Meta.Sym.Internal.mkAppRevRangeS : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Expr → ℕ → ℕ → Array Lean.Expr → m Lean.Expr
-- Mathlib.Algebra.Homology.Augment
/-- The truncation of an `ℕ`-indexed chain complex,
deleting the object at `0` and shifting everything else down.
 -/
ChainComplex.truncate : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] → CategoryTheory.Functor (ChainComplex V ℕ) (ChainComplex V ℕ)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm_assoc : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} {Y : D}
  (h : E.IsPointwiseLeftKanExtensionAt Y) {Z : H}
  (φ :
    (CategoryTheory.CostructuredArrow.proj L Y).comp F ⟶
      (CategoryTheory.Functor.const (CategoryTheory.CostructuredArrow L Y)).obj Z)
  (g : CategoryTheory.CostructuredArrow L Y) {Z_1 : H} (h_1 : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.hom E).app g.left)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.right E).map g.hom)
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.IsColimit.homEquiv h).symm φ) h_1)) =
    CategoryTheory.CategoryStruct.comp (φ.app g) h_1
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.tensor_apply : ∀ {W X Y Z : TopCat} (f : W ⟶ X) (g : Y ⟶ Z) (p : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj W Y)),
  (TopCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) p =
    ((CategoryTheory.ConcreteCategory.hom f) p.1, (CategoryTheory.ConcreteCategory.hom g) p.2)
-- Mathlib.Dynamics.Flow
/-- Restrict a flow by `τ` to a flow by an additive submonoid of `τ`.  -/
Flow.restrictAddSubmonoid : {τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] →
      [inst_1 : TopologicalSpace α] → [inst_2 : AddMonoid τ] → Flow τ α → (S : AddSubmonoid τ) → Flow (↥S) α
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- **Alias** of `Matroid.IsBasis'.contract_indep_sdiff_iff`. -/
Matroid.IsBasis'.contract_indep_diff_iff : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis' I X → ((M.contract X).Indep (J \ X) ↔ M.Indep (J \ X ∪ I))
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.refl_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂), (CategoryTheory.ShortComplex.Homotopy.refl φ).h₀ = 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {a b : α} (hab : cmp a b = Ordering.eq) {h' : a ∈ t},
  Std.DTreeMap.Raw.Const.get t a h' = Std.DTreeMap.Raw.Const.get t b ⋯
-- Mathlib.MeasureTheory.Function.Jacobian
MeasureTheory.aemeasurable_ofReal_abs_det_fderivWithin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasurableSet s →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → AEMeasurable (fun x => ENNReal.ofReal |(f' x).det|) (μ.restrict s)
-- Std.Tactic.BVDecide.LRAT.Parser
/-- Read and parse an LRAT proof from `path`. `path` may contain either the binary or the non-binary
LRAT format.
 -/
Std.Tactic.BVDecide.LRAT.loadLRATProof : System.FilePath → IO (Array Std.Tactic.BVDecide.LRAT.IntAction)
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instIsClosedUnderLimitsOfShapeFunctorOppositeTypeIsIndObjectDiscreteOfHasLimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type v}
  [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C],
  CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape CategoryTheory.Limits.IsIndObject (CategoryTheory.Discrete J)
-- Mathlib.Algebra.Group.Prod
MulHom.fst.eq_1 : ∀ (M : Type u_3) (N : Type u_4) [inst : Mul M] [inst_1 : Mul N], MulHom.fst M N = { toFun := Prod.fst, map_mul' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- The one-edge subgraph.  -/
SimpleGraph.subgraphOfAdj : {V : Type u} → (G : SimpleGraph V) → {v w : V} → G.Adj v w → G.Subgraph
-- Init.Data.Array.Lemmas
Array.foldr_add_const : ∀ {α : Type u_1} {xs : Array α} {a b : ℕ}, Array.foldr (fun x x_1 => x_1 + a) b xs = b + a * xs.size
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- `NegMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under negation.  -/
NegMemClass : (S : Type u_3) → (G : outParam (Type u_4)) → [Neg G] → [SetLike S G] → Prop
-- Init.Grind.AC
Lean.Grind.AC.Expr.toSeq_k : Lean.Grind.AC.Expr → Lean.Grind.AC.Seq
-- Lean.Meta.Tactic.Cases
_private.Lean.Meta.Tactic.Cases.0.Lean.Meta.throwInductiveTypeExpected : {α : Type} → Lean.Expr → Lean.MetaM α