mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.ne_of_adj_of_not_adj : ∀ {V : Type u} (G : SimpleGraph V) {v w x : V}, G.Adj v x → ¬G.Adj w x → v ≠ w
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.isEmpty.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Batteries.AssocList α β → Sort u_3) →
      (x : Batteries.AssocList α β) →
        (Unit → motive Batteries.AssocList.nil) →
          ((x : Batteries.AssocList α β) → (x = Batteries.AssocList.nil → False) → motive x) → motive x
-- Mathlib.Order.Ideal
/-- The ideal is upward directed.  -/
Order.Ideal.directed' : ∀ {P : Type u_2} [inst : LE P] (self : Order.Ideal P), DirectedOn (fun x1 x2 => x1 ≤ x2) self.carrier
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.ge_lower : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] (lo : ℤ),
  (i.lo? == some lo) = true → ∀ (a : α), -1 * ↑a + lo ≤ 0
-- Init.Omega.IntList
Lean.Omega.IntList.gcd_eq_iff : ∀ {xs : Lean.Omega.IntList} {g : ℕ},
  xs.gcd = g ↔ (∀ {a : ℤ}, a ∈ xs → ↑g ∣ a) ∧ ∀ (c : ℕ), (∀ {a : ℤ}, a ∈ xs → ↑c ∣ a) → c ∣ g
-- Init.MetaTypes
Lean.Meta.Simp.defaultMaxSteps : ℕ
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.mk.injEq : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {e : J}
  (prop_id : D.W (CategoryTheory.CategoryStruct.id e)) (lift : {j : J} → D.P j → (j ⟶ e))
  (hlift : ∀ {j : J} (hj : D.P j), D.W (lift hj)) (uniq : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift hj = φ)
  (comm : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), CategoryTheory.CategoryStruct.comp f (lift ⋯) = lift ⋯)
  (prop_id_1 : D.W (CategoryTheory.CategoryStruct.id e)) (lift_1 : {j : J} → D.P j → (j ⟶ e))
  (hlift_1 : ∀ {j : J} (hj : D.P j), D.W (lift_1 hj))
  (uniq_1 : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift_1 hj = φ)
  (comm_1 : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), CategoryTheory.CategoryStruct.comp f (lift_1 ⋯) = lift_1 ⋯),
  ({ prop_id := prop_id, lift := lift, hlift := hlift, uniq := uniq, comm := comm } =
      { prop_id := prop_id_1, lift := lift_1, hlift := hlift_1, uniq := uniq_1, comm := comm_1 }) =
    (lift = lift_1)
-- Mathlib.LinearAlgebra.Determinant
/-- The determinant of an endomorphism given a basis.

See `LinearMap.det` for a version that populates the basis non-computably.

Although the `Trunc (Basis ι A M)` parameter makes it slightly more convenient to switch bases,
there is no good way to generalize over universe parameters, so we can't fully state in `detAux`'s
type that it does not depend on the choice of basis. Instead you can use the `detAux_def''` lemma,
or avoid mentioning a basis at all using `LinearMap.det`.
 -/
LinearMap.detAux : {M : Type u_7} →
  [inst : AddCommGroup M] →
    {ι : Type u_8} →
      [DecidableEq ι] →
        [Fintype ι] →
          {A : Type u_9} → [inst_3 : CommRing A] → [inst_4 : Module A M] → Trunc (Module.Basis ι A M) → (M →ₗ[A] M) →* A
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.forget₂AddGroup_preservesLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.eq_def : @Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates =
  (@fun Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates._functor.call {basis} ms =>
      basis = [] ∨
        (∃ basis_hd basis_tl f,
            f =ᶠ[Filter.atTop] 0 ∧
              basis = basis_hd :: basis_tl ∧
                ms ≍
                  Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
                    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil f) ∨
          ∃ basis_hd f basis_tl exp coef tl,
            Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates._functor.call coef ∧
              Tactic.ComputeAsymptotics.Majorized f basis_hd exp ∧
                Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates._functor.call
                    (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk tl (f - basis_hd ^ exp * coef.toFun)) ∧
                  basis = basis_hd :: basis_tl ∧
                    ms ≍
                      Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
                        (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl) f)
    @Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates
-- Mathlib.Order.BoundedOrder.Basic
not_top_lt : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] {a : α}, ¬⊤ < a
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_max : Primrec₂ max
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.le_opNNNorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F) (x : E), ‖f x‖₊ ≤ ‖f‖₊ * ‖x‖₊
-- Mathlib.Data.Finset.Sups
Finset.compls_empty : ∀ {α : Type u_2} [inst : BooleanAlgebra α], ∅.compls = ∅
-- Mathlib.Algebra.Lie.Weights.Killing
/-- This is Proposition 4.18 from [carter2005] except that we use
`LieModule.exists_forall_lie_eq_smul` instead of Lie's theorem (and so avoid
assuming `K` has characteristic zero).  -/
LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L),
  (LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α) ∈ LieAlgebra.corootSpace ⇑α
-- Aesop.Index.RulePattern
/-- The name of the rule to which the pattern belongs.  -/
Aesop.RulePatternIndex.Entry.name : Aesop.RulePatternIndex.Entry → Aesop.RuleName
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
_private.Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries.0.PowerSeries.pentagonalSeries.eq_1 : ∀ (R : Type u_1) [inst : CommRing R],
  PowerSeries.pentagonalSeries R = PowerSeries.mk fun n => if h : ∃ k, pentagonal k = n then ↑↑h.choose.negOnePow else 0
-- Mathlib.Tactic.Translate.ToAdditive
/-- Maps multiplicative names to their additive counterparts.  -/
Mathlib.Tactic.ToAdditive.translations : Lean.NameMapExtension Mathlib.Tactic.Translate.TranslationInfo
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.IsLocalizationMap.exists_of_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {N : Type u_2} [inst_1 : CommMonoid N] {S : Submonoid M} {f : M → N},
  S.IsLocalizationMap f → ∀ {x y : M}, f x = f y → ∃ c, ↑c * x = ↑c * y
-- Mathlib.Analysis.Convex.Segment
segment_inter_eq_endpoint_of_linearIndependent_sub : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] [ZeroLEOneClass 𝕜] {c x y : E},
  LinearIndependent 𝕜 ![x - c, y - c] → segment 𝕜 c x ∩ segment 𝕜 c y = {c}
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
CategoryTheory.IsKernelPair.lift_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} {S : C}
  (k : CategoryTheory.IsKernelPair f a b) (p q : S ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp q f),
  CategoryTheory.CategoryStruct.comp (k.lift p q w) b = q
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Cache : Type
-- Init.Conv
/-- The `apply thm` conv tactic is the same as `apply thm` the tactic.
There are no restrictions on `thm`, but strange results may occur if `thm`
cannot be reasonably interpreted as proving one equality from a list of others.  -/
Lean.Parser.Tactic.Conv.convApply_ : Lean.ParserDescr
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.memP_def : ∀ {α : Type u_1} {cut : α → Ordering} {t : RBTree.RBNode α}, RBTree.RBNode.MemP cut t ↔ ∃ x ∈ t, cut x = Ordering.eq
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.Normal.subgroupOf : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Normal → ∀ (K : Subgroup G), (H.subgroupOf K).Normal
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow.eq_1 : ∀ (basis_hd : ℝ → ℝ) (basis_tl : Tactic.ComputeAsymptotics.Basis) (r : ℝ),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow basis_hd basis_tl 0 r =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons r Tactic.ComputeAsymptotics.MultiseriesExpansion.one
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- The spine of an `m`-simplex in `X` is the path of edges of length `m`
formed by traversing in order through its vertices.  -/
SSet.Truncated.spine : {n : ℕ} →
  (X : SSet.Truncated (n + 1)) →
    (m : ℕ) →
      (h : autoParam (m ≤ n + 1) SSet.Truncated.spine._auto_1) →
        X.obj (Opposite.op { obj := { len := m }, property := h }) → X.Path m
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.instAtPrimeSubtypeMemSubringToSubringOfPrime : ∀ {K : Type u_3} [inst : Field K] (A : Subring K) (P : Ideal ↥A) [inst_1 : P.IsPrime],
  IsLocalization.AtPrime (↥(LocalSubring.ofPrime A P).toSubring) P
-- Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
/-- Given an almost everywhere measurable function `f` with values in `ℝ≥0` in a sigma-finite space,
there exists a lower semicontinuous function `g > f` with integral arbitrarily close to that of `f`.
Formulation in terms of `lintegral`.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`.  -/
MeasureTheory.exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α)
  [μ.WeaklyRegular] [MeasureTheory.SigmaFinite μ] (f : α → NNReal),
  AEMeasurable f μ →
    ∀ {ε : ENNReal},
      ε ≠ 0 → ∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.CRingHom_eq_C : ∀ {R : Type u_1} [inst : Semiring R] {a : R} [inst_1 : MulSemiringAction (Multiplicative ℕ) R],
  SkewPolynomial.CRingHom a = SkewPolynomial.C a
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rio_succ : ∀ {n : ℕ}, (*...n + 1).toArray = (*...n).toArray ++ [n]
-- Mathlib.Algebra.Order.Group.CompleteLattice
ciSup_add : ∀ {ι : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
  [AddRightMono G], BddAbove (Set.range f) → ∀ (a : G), (⨆ i, f i) + a = ⨆ i, f i + a
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso_hom_app_hom_apply_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G H X : CategoryTheory.Functor C V)
  (a :
    (((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj (CategoryTheory.MonoidalCategory.tensor C)).comp
          (((CategoryTheory.Functor.whiskeringLeft ((C × C) × C) (C × C) V).obj
                ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C))).comp
            (CategoryTheory.coyoneda.obj
              (Opposite.op
                (CategoryTheory.MonoidalCategory.externalProduct (CategoryTheory.MonoidalCategory.externalProduct F G)
                  H))))).obj
      X)
  (X_1 : C × C × C),
  ((CategoryTheory.ConcreteCategory.hom
            ((CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso F G H).hom.app X))
          a).app
      X_1 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X_1.1) (G.obj X_1.2.1) (H.obj X_1.2.2)).inv
      (((CategoryTheory.CategoryStruct.comp
                (CategoryTheory.prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv.toIso.hom
                (TypeCat.ofHom fun g =>
                  CategoryTheory.CategoryStruct.comp g
                    (((CategoryTheory.Functor.whiskeringLeft (C × C × C) C V).map
                          (CategoryTheory.NatIso.ofComponents
                              (fun x => CategoryTheory.MonoidalCategoryStruct.associator x.1 x.2.1 x.2.2) ⋯).hom).app
                      X))).hom'
            a).app
        X_1)
-- Lean.Meta.CollectFVars
Lean.Meta.removeUnused : Array Lean.Expr → Lean.CollectFVars.State → Lean.MetaM (Lean.LocalContext × Lean.LocalInstances × Array Lean.Expr)
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.sup_covering : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (x y : CategoryTheory.Coverage C) (B : C),
  (x ⊔ y).coverings B = x.coverings B ∪ y.coverings B
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inl_map_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
  [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z_1 : C} (h : Y ⊞ Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
exp_neg_mul_rpow_isLittleO_exp_neg : ∀ {p b : ℝ}, 0 < b → 1 < p → (fun x => Real.exp (-b * x ^ p)) =o[Filter.atTop] fun x => Real.exp (-x)
-- Mathlib.LinearAlgebra.Prod
/-- Equivalence given by a block lower diagonal matrix. `e₁` and `e₂` are diagonal square blocks,
and `f` is a rectangular block below the diagonal.  -/
LinearEquiv.skewProd : {R : Type u} →
  {M : Type v} →
    {M₂ : Type w} →
      {M₃ : Type y} →
        {M₄ : Type z} →
          [inst : Semiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : AddCommGroup M₄] →
                    {module_M : Module R M} →
                      {module_M₂ : Module R M₂} →
                        {module_M₃ : Module R M₃} →
                          {module_M₄ : Module R M₄} →
                            (M ≃ₗ[R] M₂) → (M₃ ≃ₗ[R] M₄) → (M →ₗ[R] M₄) → (M × M₃) ≃ₗ[R] M₂ × M₄
-- Mathlib.Algebra.Group.TransferInstance
Equiv.neg_def : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Neg β] (x : α), -x = e.symm (-e x)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- A equality constraint and its justification/proof.  -/
Lean.Meta.Grind.Arith.Cutsat.EqCnstr : Type
-- Init.Data.Range.Basic
Std.Legacy.Range.stop : Std.Legacy.Range → ℕ
-- Mathlib.Data.Set.Countable
/-- Noncomputably enumerate elements in a set. The `default` value is used to extend the domain to
all of `ℕ`.  -/
Set.enumerateCountable : {α : Type u} → {s : Set α} → s.Countable → α → ℕ → α
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instInhabited : {α : Type u_1} → {x : MeasurableSpace α} → Inhabited (MeasureTheory.Measure α)
-- Init.Data.String.Basic
String.ofList_nil : String.ofList [] = ""
-- Init.Data.Vector.Zip
Vector.map_snd_zip : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {as : Vector α n} (bs : Vector β n), Vector.map Prod.snd (as.zip bs) = bs
-- Qq.SortLocalDecls
Qq.sortLocalDecls : Array Lean.LocalDecl → Lean.MetaM (Array Lean.LocalDecl)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.left_unitality_inv : ∀ {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) [inst_4 : F.LaxMonoidal] (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.ε F) (F.obj X))
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)) =
    F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
-- Mathlib.Topology.Sets.Opens
/-- See Note [custom simps projection].  -/
TopologicalSpace.Opens.Simps.coe : {α : Type u_2} → [inst : TopologicalSpace α] → TopologicalSpace.Opens α → Set α
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- `A` is invertible if `A.submatrix e₁ e₂` is  -/
Matrix.invertibleOfSubmatrixEquivInvertible : {m : Type u} →
  {n : Type u'} →
    {α : Type v} →
      [inst : Fintype n] →
        [inst_1 : DecidableEq n] →
          [inst_2 : CommRing α] →
            [inst_3 : Fintype m] →
              [inst_4 : DecidableEq m] →
                (A : Matrix m m α) → (e₁ e₂ : n ≃ m) → [Invertible (A.submatrix ⇑e₁ ⇑e₂)] → Invertible A
-- Mathlib.Order.Hom.Basic
OrderEmbedding.eq_iff_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β) {a b : α}, f a = f b ↔ a = b
-- Mathlib.GroupTheory.Sylow
Sylow.ext_iff : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {P Q : Sylow p G}, P = Q ↔ ↑P = ↑Q
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- `RingEquiv.quotientBot` as an algebra isomorphism.  -/
AlgEquiv.quotientBot : (R : Type u_1) → (S : Type u_2) → [inst : CommSemiring R] → [inst_1 : Ring S] → [inst_2 : Algebra R S] → (S ⧸ ⊥) ≃ₐ[R] S
-- Init.Data.Dyadic.Basic
Dyadic.instNatCast : NatCast Dyadic
-- Mathlib.Probability.Kernel.CondDistrib
/-- The conditional expectation of `Y` given `X` is almost everywhere equal to the integral
`∫ y, y ∂(condDistrib Y X μ (X a))`.  -/
ProbabilityTheory.condExp_ae_eq_integral_condDistrib' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {mβ : MeasurableSpace β} {Ω : Type u_5}
  [inst_1 : NormedAddCommGroup Ω] [inst_2 : NormedSpace ℝ Ω] [inst_3 : CompleteSpace Ω] [inst_4 : MeasurableSpace Ω]
  [inst_5 : BorelSpace Ω] [inst_6 : SecondCountableTopology Ω] {Y : α → Ω},
  Measurable X →
    MeasureTheory.Integrable Y μ →
      μ[Y | MeasurableSpace.comap X mβ] =ᵐ[μ] fun a => ∫ (y : Ω), y ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
-- Mathlib.RingTheory.Coalgebra.TensorProduct
TensorProduct.counit_tmul : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid A] [inst_3 : AddCommMonoid B] [inst_4 : Algebra R S] [inst_5 : Module R A]
  [inst_6 : Module S A] [inst_7 : Module R B] [inst_8 : IsScalarTower R S A] [inst_9 : CoalgebraStruct R B]
  [inst_10 : CoalgebraStruct S A] (x : A) (y : B),
  CoalgebraStruct.counit (x ⊗ₜ[R] y) = CoalgebraStruct.counit y • CoalgebraStruct.counit x
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Noncomputably make a colimit cocone from the existence of unique factorizations.  -/
CategoryTheory.Limits.IsColimit.ofExistsUnique : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} →
            (∀ (s : CategoryTheory.Limits.Cocone F),
                ∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) l = s.ι.app j) →
              CategoryTheory.Limits.IsColimit t
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on a field `K`, the valuation
subring defined by `v` is open in the valuative topology.  -/
Valuation.isOpen_valuationSubring : ∀ {Γ₀ : Type u_3} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_4} [inst_1 : Field K] [inst_2 : ValuativeRel K]
  [inst_3 : TopologicalSpace K] [IsValuativeTopology K] (v : Valuation K Γ₀) [v.Compatible], IsOpen ↑v.valuationSubring
-- Init.Data.List.MapIdx
List.mapFinIdx_eq_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : ℕ) → α → i < l.length → β} {g : ℕ → α → β},
  (∀ (i : ℕ) (h : i < l.length), f i l[i] h = g i l[i]) → l.mapFinIdx f = List.mapIdx g l
-- Mathlib.Data.Ordmap.Invariants
Ordnode.node3R_size : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α},
  (l.node3R x m y r).size = l.size + m.size + r.size + 2
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.interSnd_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (i : (E.inter F).I₀),
  (E.interSnd F).s₀ i = i.2
-- Mathlib.Order.Defs.Unbundled
/-- `Maximal P x` means that `x` is a maximal element satisfying `P`.  -/
Maximal : {α : Type u_1} → [LE α] → (α → Prop) → α → Prop
-- Mathlib.Data.Finset.Insert
Finset.prodPiCons.eq_1 : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α] (f : α → Type u_3) {a : α} (has : a ∉ s)
  (x : f a × ((i : α) → i ∈ s → f i)) (i : α) (hi : i ∈ Finset.cons a s has),
  Finset.prodPiCons f has x i hi = if h : i = a then cast ⋯ x.1 else x.2 i ⋯
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.isoInv_mapPullbackAdj_unit_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (T : CategoryTheory.Over X),
  ((CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f.inv).unit.app T).left = CategoryTheory.CategoryStruct.id T.left
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Equivalence.prod_functor : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D),
  (E₁.prod E₂).functor = E₁.functor.prod E₂.functor
-- Mathlib.Topology.Algebra.Support
range_eq_image_mulTSupport_or : ∀ {X : Type u_1} {α : Type u_2} [inst : One α] [inst_1 : TopologicalSpace X] (f : X → α),
  Set.range f = f '' mulTSupport f ∨ Set.range f = insert 1 (f '' mulTSupport f)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instMulRightMono : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  MulRightMono (FractionalIdeal S P)
-- Init.Data.Range.Polymorphic.Map
Std.PRange.LawfulUpwardEnumerableLeast?.ofMap : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : Std.PRange.Least? α] [inst_3 : Std.PRange.Least? β] [Std.PRange.LawfulUpwardEnumerableLeast? β]
  (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesLeast?], Std.PRange.LawfulUpwardEnumerableLeast? α
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_nsmul_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIocDiv hp a (m • p + b) = ↑m + toIocDiv hp a b
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.ofRepr.injEq : ∀ {ι : Type u_1} {G : Type u_2} [inst : AddGroup G] (repr repr_1 : G ≃+ FreeAddGroup ι),
  ({ repr := repr } = { repr := repr_1 }) = (repr = repr_1)
-- Mathlib.Analysis.Normed.Lp.MeasurableSpace
MeasurableEquiv.toLp_apply : ∀ (p : ENNReal) (X : Type u_1) [inst : MeasurableSpace X] (x : X), (MeasurableEquiv.toLp p X) x = WithLp.toLp p x