mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.uniqueAlgEquiv_symm_apply : ∀ (R : Type u_1) {A : Type u_4} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] [inst_4 : Subsingleton M] (a : A),
  (MonoidAlgebra.uniqueAlgEquiv R M).symm a = MonoidAlgebra.single 1 a
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHomEquiv_comp : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.eHomEquiv V) f)
          ((CategoryTheory.eHomEquiv V) g))
        (CategoryTheory.eComp V X Y Z))
-- Mathlib.Topology.MetricSpace.Polish
PolishSpace.IsClopenable.compl : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, PolishSpace.IsClopenable s → PolishSpace.IsClopenable sᶜ
-- Mathlib.Algebra.Group.Hom.Instances
/-- Evaluation of an `AddMonoidHom` at a point as an additive monoid homomorphism.
See also `AddMonoidHom.apply` for the evaluation of any function at a point.  -/
AddMonoidHom.eval : {M : Type uM} → {N : Type uN} → [inst : AddZeroClass M] → [inst_1 : AddCommMonoid N] → M →+ (M →+ N) →+ N
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.π₁_map : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B)
  {X Y : CategoryTheory.Limits.CategoricalPullback F G} (f : X ⟶ Y),
  (CategoryTheory.Limits.CategoricalPullback.π₁ F G).map f = f.fst
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldr_loop_succ : ∀ {n : ℕ} {α : Sort u_1} {i : ℕ} (f : Fin n → α → α) (x : α) (h : i < n),
  Fin.foldr.loop n f (i + 1) h x = Fin.foldr.loop n f i ⋯ (f ⟨i, h⟩ x)
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.subtype_symm_apply_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {q : Y → Prop}
  (h : X ≃ₜ Y) (h_iff : ∀ (x : X), p x ↔ q (h x)) (b : { b // q b }), ↑((h.subtype h_iff).symm b) = h.symm ↑b
-- Mathlib.GroupTheory.Subgroup.Centralizer
/-- The `centralizer` of `s` is the additive subgroup of `g : G` commuting with every `h : s`.  -/
AddSubgroup.centralizer : {G : Type u_1} → [inst : AddGroup G] → Set G → AddSubgroup G
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
/-- Let `A` and `C` be the adjacency matrices of a strongly regular graph with parameters `n k ℓ μ`
and its complement respectively and `I` be the identity matrix,
then `A ^ 2 = k • I + ℓ • A + μ • C`. `C` is equivalent to the expression `J - I - A`
more often found in the literature, where `J` is the all-ones matrix.  -/
SimpleGraph.IsSRGWith.matrix_eq : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ}
  [inst_2 : DecidableEq V] {α : Type u_1} [inst_3 : Semiring α],
  G.IsSRGWith n k ℓ μ →
    SimpleGraph.adjMatrix α G ^ 2 = k • 1 + ℓ • SimpleGraph.adjMatrix α G + μ • SimpleGraph.adjMatrix α Gᶜ
-- Lean.LocalContext
Lean.LocalDeclKind.default.sizeOf_spec : sizeOf Lean.LocalDeclKind.default = 1
-- Mathlib.Algebra.DirectSum.Ring
/-- Two `RingHom`s out of a direct sum are equal if they agree on the generators.  -/
DirectSum.ringHom_ext : ∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] [inst_4 : Semiring R]
  ⦃f g : (DirectSum ι fun i => A i) →+* R⦄,
  (∀ (i : ι) (x : A i), f ((DirectSum.of A i) x) = g ((DirectSum.of A i) x)) → f = g
-- Init.Data.List.Nat.TakeDrop
/-- Dropping the elements up to `l₁.length + i` in `l₁ + l₂` is the same as dropping the elements
up to `i` in `l₂`.  -/
List.drop_length_add_append : ∀ {α : Type u_1} {l₁ l₂ : List α} (i : ℕ), List.drop (l₁.length + i) (l₁ ++ l₂) = List.drop i l₂
-- Batteries.Data.DList.Lemmas
Batteries.DList.toList_singleton : ∀ {α : Type u_1} (x : α), (Batteries.DList.singleton x).toList = [x]
-- Mathlib.Data.NNReal.Defs
NNReal.coe_iSup : ∀ {ι : Sort u_2} (s : ι → NNReal), ↑(⨆ i, s i) = ⨆ i, ↑(s i)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ReferenceContext.mk.inj : ∀ {includeDeclaration includeDeclaration_1 : Bool},
  { includeDeclaration := includeDeclaration } = { includeDeclaration := includeDeclaration_1 } →
    includeDeclaration = includeDeclaration_1
-- Init.Data.Repr
hexDigitRepr : ℕ → String
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.leftCancelEquiv_comp_lTensor_comp_symm : ∀ {R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} {Q : Type u_3} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q]
  (e : TensorProduct R M N ≃ₗ[R] R) (f : P →ₗ[R] Q),
  ↑(Module.Invertible.leftCancelEquiv Q e) ∘ₗ
      LinearMap.lTensor M (LinearMap.lTensor N f) ∘ₗ ↑(Module.Invertible.leftCancelEquiv P e).symm =
    f
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.projectMapAux.eq_11 : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (W X Y Z : CategoryTheory.FreeMonoidalCategory C) (f_1 : W.Hom Y) (g : X.Hom Z),
  CategoryTheory.FreeMonoidalCategory.projectMapAux f (f_1.tensor g) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.FreeMonoidalCategory.projectMapAux f f_1)
      (CategoryTheory.FreeMonoidalCategory.projectMapAux f g)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mem_ofWithBot : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {boxes : Finset (WithBot (BoxIntegral.Box ι))} {h₁ : ∀ J ∈ boxes, J ≤ ↑I}
  {h₂ : (↑boxes).Pairwise Disjoint}, J ∈ BoxIntegral.Prepartition.ofWithBot boxes h₁ h₂ ↔ ↑J ∈ boxes
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.eq_id_of_D₂_W : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular] {ι : Type w}
  (D : ι → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ)
  (hι : HasCardinalLT ι κ) {m : J} (u : (i : ι) → (D i).top ⟶ m),
  (∀ {i : ι}, ¬(D i).P m) →
    ∀ {f : m ⟶ m},
      (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂ D hι u).W f →
        f = CategoryTheory.CategoryStruct.id m
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type v} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    ∀ [Algebra.IsAlgebraic F ↥A], Module.rank ↥A ↥(IntermediateField.extendScalars ⋯) = Module.rank F L
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- `E^n₁(f₁, f₂, f₃)` identifies to the kernel
of `δFromOpcycles : opZ^{n₁}(f₂, f₃) ⟶ H^{n₂}(f₁)`.  -/
CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (n₀ n₁ n₂ : ℤ) →
                      (hn₁ :
                          autoParam (n₀ + 1 = n₁)
                            CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex._auto_1) →
                        (hn₂ :
                            autoParam (n₁ + 1 = n₂)
                              CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex._auto_3) →
                          (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).RightHomologyData
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- A submodule is finitely generated if and only if it is finite-dimensional  -/
Submodule.fg_iff_finiteDimensional : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (s : Submodule K V),
  s.FG ↔ FiniteDimensional K ↥s
-- Mathlib.Topology.UniformSpace.Cauchy
CompleteSpace.addOpposite : ∀ {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α], CompleteSpace αᵃᵒᵖ
-- Mathlib.Order.Partition.Finpartition
Finpartition.sum_ofSubset_eq_sum : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a b : α} (P : Finpartition a) {parts : Finset α}
  (subset : parts ⊆ P.parts) (sup_parts : parts.sup id = b) {X : Type u_2} [inst_2 : AddCommMonoid X] (f : α → X),
  (∀ p ∈ P.parts, p ∉ parts → f p = 0) → ∑ p ∈ (P.ofSubset subset sup_parts).parts, f p = ∑ p ∈ P.parts, f p
-- Mathlib.Algebra.Group.Hom.Basic
/-- Negation on a commutative additive group, considered as an additive monoid
homomorphism.  -/
negAddMonoidHom : {α : Type u_1} → [inst : SubtractionCommMonoid α] → α →+ α
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_subset_inter_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, t ⊆ u → s ∩ t ⊆ s ∩ u
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- The bound on the number of polynomials used to describe the constructible set appearing in the
case of `C : R → R[X₁, ..., Xₘ]` of Chevalley's theorem with complexity bound.  -/
ChevalleyThm.MvPolynomialC.numBound : ℕ → (ℕ → ℕ) → ℕ → ℕ
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.one_add_smoothingFn_le_two : ∀ {x : ℝ}, Real.exp 1 ≤ x → 1 + AkraBazziRecurrence.smoothingFn x ≤ 2
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.enumOrd_range : ∀ {f : Ordinal.{u_1} → Ordinal.{u_1}}, StrictMono f → Ordinal.enumOrd (Set.range f) = f
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.empty : {α : Type u_1} → {β : Type u_2} → {cmp : α → α → Ordering} → Lean.PrefixTreeNode α β cmp
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonNatTrans.congr_simp : ∀ {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 F' : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] [inst_5 : F'.LaxMonoidal] (f f_1 : F ⟶ F')
  (e_f : f = f_1) [inst_6 : CategoryTheory.NatTrans.IsMonoidal f],
  CategoryTheory.Functor.mapMonNatTrans f = CategoryTheory.Functor.mapMonNatTrans f_1
-- Init.Data.List.Basic
List.reverseAux_reverseAux : ∀ {α : Type u} {as bs cs : List α}, (as.reverseAux bs).reverseAux cs = bs.reverseAux ((as.reverseAux []).reverseAux cs)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
posMulMono_iff_mulPosMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [IsMulCommutative α],
  PosMulMono α ↔ MulPosMono α
-- Mathlib.RingTheory.Algebraic.Basic
isAlgebraic_algHom_iff : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u_2}
  [inst_3 : Ring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
  Function.Injective ⇑f → ∀ {a : A}, IsAlgebraic R (f a) ↔ IsAlgebraic R a
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.lowerEquivalence_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : C} {B : D} (e : CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B),
  (CategoryTheory.Subobject.lowerEquivalence e).functor = CategoryTheory.Subobject.lower e.functor
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_eq_some_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  (he : t ≠ ∅), t.maxKey? = some (t.maxKey he)
-- Mathlib.Algebra.Algebra.Operations
Submodule.mem_mul_span_singleton : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] {P : Submodule R A}
  {x y : A}, x ∈ P * (R ∙ y) ↔ ∃ z ∈ P, z * y = x
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isEmpty_dropEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String.Slice},
  (s.dropEndWhile pat).isEmpty = s.revAll pat
-- Mathlib.Combinatorics.Additive.Dissociation
/-- **Alias** of the forward direction of `mulDissociated_inv`. -/
MulDissociated.of_inv : ∀ {α : Type u_1} [inst : CommGroup α] {s : Set α}, MulDissociated s⁻¹ → MulDissociated s
-- Mathlib.Topology.Order.AtTopBotIxx
map_coe_Iio_atTop : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] (a : X),
  autoParam (Order.IsSuccPrelimit a) map_coe_Iio_atTop._auto_1 →
    Filter.map Subtype.val Filter.atTop = nhdsWithin a (Set.Iio a)
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.Hom.ofRel.injEq : ∀ {X Y : CategoryTheory.RelCat} (rel rel_1 : SetRel X Y), ({ rel := rel } = { rel := rel_1 }) = (rel = rel_1)
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.instMembership : {G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} →
      [inst : Group G] →
        [inst_1 : MulAction G X] → {ps : DiscreteTiling.Protoset G X ιₚ} → Membership X (DiscreteTiling.PlacedTile ps)
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.Factors.ne_bot : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : IsDedekindDomain S] (P : ↥(UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset),
  ↑P ≠ ⊥
-- Mathlib.Topology.UniformSpace.Completion
/-- Extend a two variable map to the Hausdorff completions.  -/
UniformSpace.Completion.extension₂ : {α : Type u_1} →
  [inst : UniformSpace α] →
    {β : Type u_2} →
      [inst_1 : UniformSpace β] →
        {γ : Type u_3} → [UniformSpace γ] → (α → β → γ) → UniformSpace.Completion α → UniformSpace.Completion β → γ
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category `C` which has filtered colimits of a given size is said to have `AB5` of that size
provided that these filtered colimits are exact.

`AB5OfSize.{w, w'} C` means that `C` has exact colimits of shape `J : Type w'` with
`Category.{w} J` such that `J` is filtered.
 -/
CategoryTheory.AB5OfSize : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w', v, u} C] → Prop
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.FiniteMeasure.prod_prod : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) (s : Set α) (t : Set β),
  (μ.prod ν) (s ×ˢ t) = μ s * ν t
-- Lean.DocString.Links
/-- Maps `lean-manual` URL paths to their corresponding manual domains.  -/
_private.Lean.DocString.Links.0.Lean.domainMap : Std.HashMap String String
-- Qq.Typ
Qq.instToStringQuoted : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
-- Mathlib.Data.Bool.Basic
Bool.or_eq_false_eq_eq_false_and_eq_false : ∀ (a b : Bool), ((a || b) = false) = (a = false ∧ b = false)
-- Mathlib.Algebra.Lie.Killing
LieAlgebra.IsKilling.instSemisimple : ∀ (K : Type u_2) (L : Type u_3) [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [Module.Finite K L], LieAlgebra.IsSemisimple K L
-- Std.Time.Internal.Bounded
_private.Std.Time.Internal.Bounded.0.Int.tdiv.match_1.splitter : (motive : ℤ → ℤ → Sort u_1) →
  (x x_1 : ℤ) →
    ((m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) →
      ((m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) →
        ((m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n)) →
          ((m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)) → motive x x_1
-- Init.Data.List.Find
List.lookup_eq_some_iff : ∀ {α : Type u_2} [inst : BEq α] {β : Type u_1} [LawfulBEq α] {l : List (α × β)} {k : α} {b : β},
  List.lookup k l = some b ↔ ∃ l₁ l₂, l = l₁ ++ (k, b) :: l₂ ∧ ∀ p ∈ l₁, (k != p.1) = true
-- Init.Data.String.Basic
String.endExclusive_sliceTo : ∀ {s : String} {p : s.Pos}, (s.sliceTo p).endExclusive = p
-- Init.WF
Prod.RProd.intro : ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} {b₁ : β} {a₂ : α} {b₂ : β},
  ra a₁ a₂ → rb b₁ b₂ → Prod.RProd ra rb (a₁, b₁) (a₂, b₂)
-- Mathlib.Order.Filter.IsBounded
Filter.isBounded_principal : ∀ {α : Type u_1} {r : α → α → Prop} (s : Set α), Filter.IsBounded r (Filter.principal s) ↔ ∃ t, ∀ x ∈ s, r x t
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.homMk'_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {Y' Y'' : C} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) (g : Y' ⟶ f.left)
  (g' : Y'' ⟶ Y'),
  f.homMk' (CategoryTheory.CategoryStruct.comp g' g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f.hom)).homMk' g')
        (f.homMk' g))
-- Mathlib.Analysis.Convex.Jensen
/-- Concave **Jensen's inequality**, `Finset.sum` version.  -/
ConcaveOn.le_map_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  ConcaveOn 𝕜 s f →
    (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ i ∈ t, p i ∈ s) → ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.gluedTo_injective : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), Function.Injective ⇑I.gluedTo
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₁.ιLeft_comp_t : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] {X Y : C} (f : X ⟶ Y)
  (hf : W f) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.D₁.ιLeft f hf g)
      (CategoryTheory.OrthogonalReflection.D₁.t W Z) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.OrthogonalReflection.D₁.ιRight f hf g)
-- Mathlib.Algebra.Algebra.Hom
/-- `AlgebraMap` as an `AlgHom`.  -/
Algebra.ofId : (R : Type u) → (A : Type v) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → R →ₐ[R] A
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.instAddActionSubtypeAEEqFunMemAddAddSubgroupLp.eq_1 : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : AddMonoid M] [inst_3 : AddAction M α]
  [inst_4 : MeasureTheory.VAddInvariantMeasure M α μ] [inst_5 : MeasurableConstVAdd M α],
  DomAddAct.instAddActionSubtypeAEEqFunMemAddAddSubgroupLp = Function.Injective.addAction Subtype.val ⋯ ⋯
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trNormal.match_1.eq_5 : ∀ (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) (f g : Turing.ToPartrec.Code)
  (k : Turing.PartrecToTM2.Cont') (h_1 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k)
  (h_2 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k)
  (h_3 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k)
  (h_4 : (f fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k)
  (h_5 : (f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k)
  (h_6 : (f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k)
  (h_7 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive f.fix k),
  (match f.comp g, k with
    | Turing.ToPartrec.Code.zero', k => h_1 k
    | Turing.ToPartrec.Code.succ, k => h_2 k
    | Turing.ToPartrec.Code.tail, k => h_3 k
    | f.cons fs, k => h_4 f fs k
    | f.comp g, k => h_5 f g k
    | f.case g, k => h_6 f g k
    | f.fix, k => h_7 f k) =
    h_5 f g k
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Equivalence.induced_inverse_obj : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) (a : D),
  (CategoryTheory.Equivalence.induced e).inverse.obj a = e.symm a
-- Mathlib.Order.Filter.Finite
/-- **Alias** of `Filter.frequently_exists_finset`. -/
Finset.frequently_exists : ∀ {α : Type u} {ι : Type u_2} (I : Finset ι) {l : Filter α} {p : ι → α → Prop},
  (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
-- Mathlib.Analysis.Calculus.Deriv.Basic
deriv_const' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (c : F), (deriv fun x => c) = fun x => 0
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.id_map : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {X Y : B} (f : X ⟶ Y),
  (CategoryTheory.StrictlyUnitaryLaxFunctor.id B).map f = f
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Presentation.toIsPresentation : ∀ {A : Type u} [inst : Ring A] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module A M]
  (self : Module.Presentation A M), self.IsPresentation
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.strictMono_comap_prod_map : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M),
  StrictMono fun m => (Submodule.comap p.subtype m, Submodule.map p.mkQ m)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.CoconeMorphism.mk.congr_simp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cocone F} (hom hom_1 : A.pt ⟶ B.pt)
  (e_hom : hom = hom_1) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι.app j) hom = B.ι.app j),
  { hom := hom, w := w } = { hom := hom_1, w := ⋯ }
-- Mathlib.Logic.Equiv.Defs
Equiv.eq_symm_comp : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : γ → α) (g : γ → β), f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
-- Mathlib.Algebra.Order.Field.Basic
_private.Mathlib.Algebra.Order.Field.Basic.0.exists_lt_mul_right_of_nonneg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b c : α},
  0 ≤ a → 0 ≤ c → c < a * b → ∃ b' ∈ Set.Ico 0 b, c < a * b'
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.CastMode.proofs.sizeOf_spec : sizeOf Mathlib.Tactic.DepRewrite.CastMode.proofs = 1
-- Mathlib.Algebra.Module.LinearMap.Index
LinearMap.index_neg : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {k : Type u_3}
  [inst_2 : DivisionRing k] [inst_3 : Module k M] [inst_4 : Module k N] {f : M →ₗ[k] N}, (-f).index = f.index
-- Mathlib.Data.Nat.Log
Nat.log_of_one_lt_of_le : ∀ {b n : ℕ}, 1 < b → b ≤ n → Nat.log b n = Nat.log b (n / b) + 1