mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Independent
/-- A subset of a convex independent set of points is convex independent as well.  -/
ConvexIndependent.mono : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s t : Set E}, ConvexIndependent 𝕜 Subtype.val → s ⊆ t → ConvexIndependent 𝕜 Subtype.val
-- Mathlib.Analysis.Convex.Function
StrictConvexOn.sub_concaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f g : E → β}, StrictConvexOn 𝕜 s f → ConcaveOn 𝕜 s g → StrictConvexOn 𝕜 s (f - g)
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- **Alias** of `CategoryTheory.Limits.Types.isTerminalPUnit`.

---

The terminal object in `Type u` is `PUnit`.  -/
CategoryTheory.Limits.Types.isTerminalPunit : CategoryTheory.Limits.IsTerminal PUnit.{u + 1}
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.unop_f₂₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ), sq.unop.f₂₄ = sq.f₁₂.unop
-- Mathlib.Analysis.Complex.LocallyUniformLimit
Complex.norm_cderiv_lt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {z : ℂ} {M r : ℝ} {f : ℂ → E},
  0 < r → (∀ w ∈ Metric.sphere z r, ‖f w‖ < M) → ContinuousOn f (Metric.sphere z r) → ‖Complex.cderiv r f z‖ < M / r
-- Mathlib.LinearAlgebra.Prod
LinearMap.kerComplementEquivRange_symm_apply : ∀ {R : Type u_3} {M : Type u_4} {M₂ : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂) {C : Submodule R M} (h : IsCompl C f.ker)
  (a : ↥f.range),
  (f.kerComplementEquivRange h).symm a =
    (LinearEquiv.ofInjective (LinearMap.codRestrict f.range (f ∘ₗ C.subtype) ⋯) ⋯).symm
      ((LinearEquiv.ofTop (LinearMap.codRestrict f.range (f ∘ₗ C.subtype) ⋯).range ⋯).symm a)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.hasPushout_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂)
  (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂]
  [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄]
  [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂))
      g₄],
  CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
SzemerediRegularity.star.eq_1 : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} (hP : P.IsEquipartition)
  (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj] (ε : ℝ) {U : Finset α} (hU : U ∈ P.parts) (V : Finset α),
  SzemerediRegularity.star hP G ε hU V =
    {A ∈ (SzemerediRegularity.chunk hP G ε hU).parts | A ⊆ G.nonuniformWitness ε U V}
-- Mathlib.CategoryTheory.Limits.FinallySmall
/-- A category is `FinallySmall.{w}` if there is a final functor from a `w`-small category.  -/
CategoryTheory.FinallySmall : (J : Type u) → [CategoryTheory.Category.{v, u} J] → Prop
-- Mathlib.Logic.OpClass
/-- `RightCommutative op` where `op : β → α → β` says that `op` is a right-commutative operation,
i.e. `op (op b a₁) a₂ = op (op b a₂) a₁`.  -/
RightCommutative : {α : Sort u} → {β : Sort v} → (β → α → β) → Prop
-- Mathlib.Topology.FiberBundle.Constructions
FiberBundle.pullback_trivializationAt' : ∀ {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : TopologicalSpace F] [inst_3 : TopologicalSpace B]
  [inst_4 : ∀ (_b : B), Nonempty (E _b)] {K : Type U} [inst_5 : FunLike K B' B] [inst_6 : ContinuousMapClass K B' B]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E] (f : K) (x : B'),
  FiberBundle.trivializationAt' x = (trivializationAt F E (f x)).pullback f
-- Mathlib.Tactic.Order.ToInt
Mathlib.Tactic.Order.ToInt.toInt_le_toInt : ∀ {α : Type u_1} [inst : LinearOrder α] {n : ℕ} (val : Fin n → α) (i j : Fin n),
  Mathlib.Tactic.Order.ToInt.toInt val i ≤ Mathlib.Tactic.Order.ToInt.toInt val j ↔ val i ≤ val j
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_empty : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F},
  μ ∅ = 0
-- Mathlib.MeasureTheory.Measure.PreVariation
/-- A `Finpartition` constructor in the subtype of `MeasurableSet` from a `P : Finpartition s` with
explicit measurability assumptions.  -/
Finpartition.toMeasurableSet : {X : Type u_1} →
  [inst : MeasurableSpace X] →
    {s : Set X} →
      (P : Finpartition s) → (hs : MeasurableSet s) → (∀ p ∈ P.parts, MeasurableSet p) → Finpartition ⟨s, hs⟩
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.EqInfo.hyp.sizeOf_spec : ∀ (fvarId : Lean.FVarId), sizeOf (Lean.Meta.EqInfo.hyp✝ fvarId) = 1 + sizeOf fvarId
-- Mathlib.CategoryTheory.Action.Limits
Action.instHasFiniteCoproducts : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [CategoryTheory.Limits.HasFiniteCoproducts V], CategoryTheory.Limits.HasFiniteCoproducts (Action V G)
-- Mathlib.Data.FP.Basic
FP.instDecidableValidFinite : [C : FP.FloatCfg] → (e : ℤ) → (m : ℕ) → Decidable (FP.ValidFinite e m)
-- Std.Internal.Do.WP.Basic
/-- Variant of `map_le_wp_map` with an explicit postcondition equality hypothesis.  -/
Std.Internal.Do.WPMonad.map_le_wp_map' : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type z} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α β : Type u} (f : α → β)
  (x : m α) (post : α → Pred) (post' : β → Pred) (epost : EPred),
  (post = fun a => post' (f a)) →
    Lean.Order.PartialOrder.rel (Std.Internal.Do.wp x post epost) (Std.Internal.Do.wp (f <$> x) post' epost)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instIsIsoCommRingCatInvApp : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (U : TopologicalSpace.Opens ↑X.toTopCat),
  CategoryTheory.IsIso (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f U)
-- Mathlib.Order.Category.PartOrdEmb
/-- The colimit cocone for a functor `F : J ⥤ PartOrdEmb` from a filtered
category that is constructed from a colimit cocone for `F ⋙ forget _`.  -/
PartOrdEmb.Limits.cocone : {J : Type u} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] →
      {F : CategoryTheory.Functor J PartOrdEmb} →
        {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))} →
          CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.Cocone F
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_list : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {xs : List α} {init : β} {f : α → β → m (ForInStep β)}
  (inv : Std.Internal.Do.Invariant xs β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs, property := ⋯ } init ⦄ forIn xs init f ⦃ fun b =>
      inv { «prefix» := xs, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
_private.Mathlib.NumberTheory.DiophantineApproximation.Basic.0.Real.convergent.match_1.eq_1 : ∀ (motive : ℝ → ℕ → Sort u_1) (ξ : ℝ) (h_1 : (ξ : ℝ) → motive ξ 0) (h_2 : (ξ : ℝ) → (n : ℕ) → motive ξ n.succ),
  (match ξ, 0 with
    | ξ, 0 => h_1 ξ
    | ξ, n.succ => h_2 ξ n) =
    h_1 ξ
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.equivMvPolynomial_symm_C : ∀ {R : Type u_1} [inst : CommSemiring R] (a : R),
  (Polynomial.Bivariate.equivMvPolynomial R).symm (MvPolynomial.C a) = Polynomial.C (Polynomial.C a)
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Subgroup.subgroupOfContinuousMulEquivOfLe.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {H K : Subgroup G} (hHK : H ≤ K),
  Subgroup.subgroupOfContinuousMulEquivOfLe hHK = (Subgroup.subgroupOfEquivOfLe hHK).toContinuousMulEquiv ⋯
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.isCentralScalar : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N : LieSubmodule R L M} {S : Type u_1} [inst_5 : Semiring S]
  [inst_6 : SMul S R] [inst_7 : Module S M] [inst_8 : IsScalarTower S R M] [inst_9 : SMul Sᵐᵒᵖ R]
  [inst_10 : Module Sᵐᵒᵖ M] [inst_11 : IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M], IsCentralScalar S (M ⧸ N)
-- Mathlib.GroupTheory.Sylow
/-- If a Sylow `p`-subgroup has finite index, then the number of Sylow `p`-subgroups is finite.  -/
Sylow.finite_of_finiteIndex : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (P : Sylow p G) [(↑P).FiniteIndex], Finite (Sylow p G)
-- Init.Data.BitVec.Lemmas
BitVec.saddOverflow.eq_1 : ∀ {w : ℕ} (x y : BitVec w),
  x.saddOverflow y = (decide (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || decide (x.toInt + y.toInt < -2 ^ (w - 1)))
-- Mathlib.Algebra.MvPolynomial.SchwartzZippel
/-- The **Schwartz-Zippel lemma**

For a nonzero multivariable polynomial `p` over an integral domain, the probability that `p`
evaluates to zero at points drawn at random from some finite subset `S` of the integral domain is
bounded by the degree of `p` over `#S`. This version presents this lemma in terms of `Finset`.  -/
MvPolynomial.schwartz_zippel_totalDegree : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [inst_2 : DecidableEq R] {n : ℕ} {p : MvPolynomial (Fin n) R},
  p ≠ 0 →
    ∀ (S : Finset R),
      ↑{f ∈ Fintype.piFinset fun x => S | (MvPolynomial.eval f) p = 0}.card / ↑S.card ^ n ≤ ↑p.totalDegree / ↑S.card
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
List.prod_nonneg : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {s : List R},
  (∀ a ∈ s, 0 ≤ a) → 0 ≤ s.prod
-- Mathlib.Algebra.GradedMonoid
/-- Each grade `A i` derives an `A 0`-action structure from `GMonoid A`.  -/
GradedMonoid.GradeZero.mulAction : {ι : Type u_1} →
  (A : ι → Type u_2) → [inst : AddMonoid ι] → [inst_1 : GradedMonoid.GMonoid A] → {i : ι} → MulAction (A 0) (A i)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State.mk.inj : ∀ {bottomUps higherOrders funBinders provideds : Array Bool} {namedArgs : Array Lean.Name}
  {bottomUps_1 higherOrders_1 funBinders_1 provideds_1 : Array Bool} {namedArgs_1 : Array Lean.Name},
  { bottomUps := bottomUps, higherOrders := higherOrders, funBinders := funBinders, provideds := provideds,
        namedArgs := namedArgs } =
      { bottomUps := bottomUps_1, higherOrders := higherOrders_1, funBinders := funBinders_1, provideds := provideds_1,
        namedArgs := namedArgs_1 } →
    bottomUps = bottomUps_1 ∧
      higherOrders = higherOrders_1 ∧ funBinders = funBinders_1 ∧ provideds = provideds_1 ∧ namedArgs = namedArgs_1
-- Mathlib.Topology.Category.TopCat.Basic
/-- The underlying type.  -/
TopCat.carrier : TopCat → Type u
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffWithinAt_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {s : Set M} {x : M}
  {n : WithTop ℕ∞} {c : M'}, ContMDiffWithinAt I I' n (fun x => c) s x
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- **Alias** of `AlgebraicGeometry.tilde`.

---

`M^~` as a sheaf of `𝒪_{Spec R}`-modules
 -/
ModuleCat.tilde : {R : CommRingCat} → ModuleCat ↑R → (AlgebraicGeometry.Spec R).Modules
-- Mathlib.Algebra.MvPolynomial.Supported
/-- The set of polynomials whose variables are contained in `s` as a `Subalgebra` over `R`.  -/
MvPolynomial.supported : {σ : Type u_1} → (R : Type u) → [inst : CommSemiring R] → Set σ → Subalgebra R (MvPolynomial σ R)
-- Mathlib.Algebra.Order.Floor.Defs
/-- A `FloorRing` constructor from the `floor` function alone.  -/
FloorRing.ofFloor : (α : Type u_4) →
  [inst : Ring α] →
    [inst_1 : LinearOrder α] → [IsOrderedRing α] → (floor : α → ℤ) → GaloisConnection Int.cast floor → FloorRing α
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.constFormalMultilinearSeries_radius : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {v : F},
  (constFormalMultilinearSeries 𝕜 E v).radius = ⊤
-- Mathlib.Computability.Reduce
OneOneReducible.trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {p : α → Prop} {q : β → Prop} {r : γ → Prop}, p ≤₁ q → q ≤₁ r → p ≤₁ r
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Coinductive predicate stating that `ms` approximates its attached function on `basis`.
* If `basis = []`, i.e. `ms` is just a real number, `Approximates` holds unconditionally.
* If `basis = basis_hd :: basis_tl` and `ms = nil`, then `f =ᶠ[atTop] 0`.
* If `basis = basis_hd :: basis_tl` and `ms = cons exp coef tl`, then
  `f` is `Majorized` with exponent `exp` by `basis_hd`,
  `coef` approximates its attached function, and
  `tl` approximates `f - basis_hd ^ exp * coef.toFun`.
 -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates : {basis : Tactic.ComputeAsymptotics.Basis} → Tactic.ComputeAsymptotics.MultiseriesExpansion basis → Prop
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J] {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (i : J) (hi : i < j),
  (CategoryTheory.SmallObject.SuccStruct.ofCocone c).obj ⟨i, ⋯⟩ = F.obj ⟨i, hi⟩
-- Mathlib.Algebra.Group.Action.Units
AddUnits.instVAddAssocClass : ∀ {M : Type u_3} {N : Type u_4} {α : Type u_5} [inst : AddMonoid M] [inst_1 : VAdd M N] [inst_2 : VAdd M α]
  [inst_3 : VAdd N α] [VAddAssocClass M N α], VAddAssocClass (AddUnits M) N α
-- Mathlib.MeasureTheory.Covering.DensityTheorem
IsUnifLocDoublingMeasure.scalingScaleOf.congr_simp : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ μ_1 : MeasureTheory.Measure α)
  (e_μ : μ = μ_1) [inst_2 : IsUnifLocDoublingMeasure μ] (K K_1 : ℝ),
  K = K_1 → IsUnifLocDoublingMeasure.scalingScaleOf μ K = IsUnifLocDoublingMeasure.scalingScaleOf μ_1 K_1
-- Mathlib.Probability.Process.Predictable
/-- **Alias** of `MeasureTheory.IsStronglyPredictable.measurable_add_one`.

---

If `u` is a discrete predictable process, then `u (n + 1)` is `𝓕 n`-measurable.  -/
MeasureTheory.IsPredictable.measurable_add_one : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_3} [inst : TopologicalSpace E] {𝓕 : MeasureTheory.Filtration ℕ m}
  {u : ℕ → Ω → E}, MeasureTheory.IsStronglyPredictable 𝓕 u → ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (u (n + 1))
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.ofHom_comp : ∀ {X Y Z : Type u} [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] [inst_2 : AddCommGroup Z] (f : X →+ Y)
  (g : Y →+ Z),
  AddCommGrpCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (AddCommGrpCat.ofHom f) (AddCommGrpCat.ofHom g)
-- Mathlib.Algebra.Group.Action.Defs
MulDistribMulAction.ext_iff : ∀ {M : Type u_9} {N : Type u_10} {inst : Monoid M} {inst_1 : Monoid N} {x y : MulDistribMulAction M N},
  x = y ↔ SMul.smul = SMul.smul
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.postcompose₂_map_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {E : Type u_7} [inst_2 : CategoryTheory.Category.{v_7, u_7} E]
  {E' : Type u_8} [inst_3 : CategoryTheory.Category.{v_8, u_8} E'] {X Y : CategoryTheory.Functor E E'} (f : X ⟶ Y)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) (c : C₁) (c_1 : C₂),
  (((CategoryTheory.Functor.postcompose₂.map f).app F).app c).app c_1 = f.app ((F.obj c).obj c_1)
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `{ m_i }` is an `R`-basis of `M`, if `{ n_j }` is an `R`-basis of `N`,
such that the family `{ m_i * n_j }` in `S` is `R`-linearly independent,
then `M` and `N` are linearly disjoint.  -/
Submodule.LinearDisjoint.of_basis_mul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (M N : Submodule R S)
  {κ : Type u_1} {ι : Type u_2} (m : Module.Basis κ R ↥M) (n : Module.Basis ι R ↥N),
  (LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)) → M.LinearDisjoint N
-- Mathlib.Data.QPF.Univariate.Basic
QPF.liftp_iff' : ∀ {F : Type u → Type v} [q : QPF F] {α : Type u} (p : α → Prop) (x : F α),
  Functor.Liftp p x ↔ ∃ u, QPF.abs u = x ∧ ∀ (i : (QPF.P F).B u.fst), p (u.snd i)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β},
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) ↔ ∃ c, (a, b, c) ∈ t
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceInlayHintParams : Lean.Lsp.FileSource Lean.Lsp.InlayHintParams
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourier_real_eq : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E) (w : ℝ),
  FourierTransform.fourier f w = ∫ (v : ℝ), Real.fourierChar (-(v * w)) • f v
-- Mathlib.GroupTheory.Solvable
Group.isSolvable_iff_commutator_lt : ∀ {G : Type u_1} [inst : Group G] [WellFoundedLT (Subgroup G)],
  Group.IsSolvable G ↔ ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticFinishedSnapshot.mk.injEq : ∀ (toSnapshot : Lean.Language.Snapshot) (state? : Option Lean.Elab.Tactic.SavedState)
  (moreSnaps : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) (toSnapshot_1 : Lean.Language.Snapshot)
  (state?_1 : Option Lean.Elab.Tactic.SavedState)
  (moreSnaps_1 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)),
  ({ toSnapshot := toSnapshot, state? := state?, moreSnaps := moreSnaps } =
      { toSnapshot := toSnapshot_1, state? := state?_1, moreSnaps := moreSnaps_1 }) =
    (toSnapshot = toSnapshot_1 ∧ state? = state?_1 ∧ moreSnaps = moreSnaps_1)
-- Init.Data.Array.MinMax
Array.min_eq_get_min? : ∀ {α : Type u_1} [inst : Min α] (xs : Array α) (h : xs ≠ #[]), xs.min h = xs.min?.get ⋯
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Nat.Icc_eq_empty_of_lt : ∀ {m n : ℕ}, n.blt m = true → Finset.Icc m n = ∅
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromCols_inj : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7}, Function.Injective2 Matrix.fromCols
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.mk.sizeOf_spec : ∀ {R : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : SizeOf R] (toAddGroupSeminorm : AddGroupSeminorm R)
  (mul_le' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) ≤ toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y),
  sizeOf { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' } = 1 + sizeOf toAddGroupSeminorm
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_of_contains_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α},
  (t.erase k).contains a = true → t.contains a = true
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.add_closedBall : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → ∀ (x : E), s + Metric.closedBall x δ = x +ᵥ Metric.cthickening δ s
-- Mathlib.Algebra.Lie.TraceForm
LieIdeal.killingForm_eq : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R],
  killingForm R ↥I = (killingForm R L).restrict (LieIdeal.toLieSubalgebra R L I).toSubmodule
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
/-- The conditional cdf is a strongly measurable function of `a : α` for all `x : ℝ`.  -/
ProbabilityTheory.stronglyMeasurable_condCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (x : ℝ),
  MeasureTheory.StronglyMeasurable fun a => ↑(ProbabilityTheory.condCDF ρ a) x
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- The map (as a cone) of a pullback cone is limit iff
the map (as a pullback cone) is limit.  -/
CategoryTheory.Limits.PullbackCone.isLimitMapConeEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X Y Z : C} →
          {f : X ⟶ Z} →
            {g : Y ⟶ Z} →
              (c : CategoryTheory.Limits.PullbackCone f g) →
                (G : CategoryTheory.Functor C D) →
                  CategoryTheory.Limits.IsLimit (G.mapCone c) ≃ CategoryTheory.Limits.IsLimit (c.map G)
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.instAddConstMapClass : ∀ {G : Type u_4} {H : Type u_5} [inst : Add G] [inst_1 : Add H] {a : G} {b : H},
  AddConstMapClass (AddConstEquiv G H a b) G H a b
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
/-- If `A` is qualified as an adjacency matrix,
then the adjacency matrix of the graph induced by `A` is itself.  -/
Matrix.IsAdjMatrix.adjMatrix_toGraph_eq : ∀ {α : Type u_1} {V : Type u_2} [inst : MulZeroOneClass α] [inst_1 : Nontrivial α] {A : Matrix V V α}
  (h : A.IsAdjMatrix) [inst_2 : DecidableEq α], SimpleGraph.adjMatrix α h.toGraph = A