mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g f) h
-- Mathlib.Algebra.Module.ULift
ULift.distribMulAction : {R : Type u} →
  {M : Type v} →
    [inst : Monoid R] → [inst_1 : AddMonoid M] → [DistribMulAction R M] → DistribMulAction (ULift.{u_1, u} R) M
-- Mathlib.Algebra.Algebra.Operations
/-- `Submodule.pow_succ` with the right-hand side commuted.  -/
Submodule.pow_succ' : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M : Submodule R A) {n : ℕ}, n ≠ 0 → M ^ (n + 1) = M * M ^ n
-- Mathlib.Order.Interval.Set.Basic
/-- **Alias** of `Set.self_notMem_Iio`. -/
Set.notMem_Iio_self : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, a ∉ Set.Iio a
-- Lean.Data.Lsp.Workspace
Lean.Lsp.DidChangeWatchedFilesRegistrationOptions.watchers : Lean.Lsp.DidChangeWatchedFilesRegistrationOptions → Array Lean.Lsp.FileSystemWatcher
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factorThru_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Subobject X)
  (h : P.Factors P.arrow),
  P.factorThru P.arrow h = CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.obj P)
-- Init.Data.RArray
Lean.RArray.getImpl.eq_2 : ∀ {α : Type u} (n p : ℕ) (l r : Lean.RArray α),
  (Lean.RArray.branch p l r).getImpl n = if n < p then l.getImpl n else r.getImpl n
-- Mathlib.Order.Monotone.Monovary
antivary_const_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (f : ι → α) (b : β),
  Antivary f (Function.const ι b)
-- Mathlib.Algebra.DirectSum.Decomposition
/-- A decomposition is an equivalence between an additive monoid `M` and a direct sum of additive
submonoids `ℳ i` of that `M`, such that the "recomposition" is canonical. This definition also
works for additive groups and modules.

This is a version of `DirectSum.IsInternal` which comes with a constructive inverse to the
canonical "recomposition" rather than just a proof that the "recomposition" is bijective.

Often it is easier to construct a term of this type via `Decomposition.ofAddHom` or
`Decomposition.ofLinearMap`.  -/
DirectSum.Decomposition : {ι : Type u_1} →
  {M : Type u_3} →
    {σ : Type u_4} →
      [DecidableEq ι] →
        [inst : AddCommMonoid M] → [inst_1 : SetLike σ M] → [AddSubmonoidClass σ M] → (ι → σ) → Type (max u_1 u_3)
-- Lean.PrivateName
_private.Lean.PrivateName.0.Lean.isPrivatePrefix.go : Lean.Name → Bool
-- Mathlib.Combinatorics.Quiver.Push
/-- The `Quiver` instance obtained by pushing arrows of `V` along the map `σ : V → W`  -/
Quiver.Push : {V : Type u_1} → {W : Type u_2} → (V → W) → Type u_2
-- Mathlib.Analysis.Normed.Group.Quotient
NormedAddGroupHom.lift_unique : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {N : Type u_3} [inst_1 : SeminormedAddCommGroup N]
  (S : AddSubgroup M) (f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0) (g : NormedAddGroupHom (M ⧸ S) N),
  g.comp S.normedMk = f → g = NormedAddGroupHom.lift S f hf
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.eq_4 : ∀ (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) (distance : ℕ) (h_1 : Unit → motive Std.Tactic.BVDecide.BVUnOp.not)
  (h_2 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance))
  (h_3 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance))
  (h_4 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance))
  (h_5 : Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) (h_6 : Unit → motive Std.Tactic.BVDecide.BVUnOp.clz)
  (h_7 : Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop),
  (match Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance with
    | Std.Tactic.BVDecide.BVUnOp.not => h_1 ()
    | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance => h_2 distance
    | Std.Tactic.BVDecide.BVUnOp.rotateRight distance => h_3 distance
    | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance => h_4 distance
    | Std.Tactic.BVDecide.BVUnOp.reverse => h_5 ()
    | Std.Tactic.BVDecide.BVUnOp.clz => h_6 ()
    | Std.Tactic.BVDecide.BVUnOp.cpop => h_7 ()) =
    h_4 distance
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.reverse_reverse : ∀ {V : Type u_2} [inst : Quiver V] [h : Quiver.HasInvolutiveReverse V] {a b : V} (f : a ⟶ b),
  Quiver.reverse (Quiver.reverse f) = f
-- Init.Control.StateCps
StateCpsT.runK_pure : ∀ {α σ : Type u} {m : Type u → Type v} {β : Type u} (a : α) (s : σ) (k : α → σ → m β), (pure a).runK s k = k a s
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseMarkerNarrow : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.HourMarker
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_mul : ∀ (x : NNReal) (y z : ℝ), x ^ (y * z) = (x ^ y) ^ z
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.RetractArrow.rightLiftingProperty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z W X' Y' : C} {f : X ⟶ Y} {f' : X' ⟶ Y'}
  (h : CategoryTheory.RetractArrow f' f) (g : Z ⟶ W) [CategoryTheory.HasLiftingProperty g f],
  CategoryTheory.HasLiftingProperty g f'
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.symm_mapRingEquiv`. -/
MonoidAlgebra.symm_mapRangeRingEquiv : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (e : R ≃+* S), (MonoidAlgebra.mapRingEquiv M e).symm = MonoidAlgebra.mapRingEquiv M e.symm
-- Mathlib.Algebra.Group.Submonoid.Membership
FreeAddMonoid.mrange_lift : ∀ {M : Type u_1} [inst : AddMonoid M] {α : Type u_4} (f : α → M),
  AddMonoidHom.mrange (FreeAddMonoid.lift f) = AddSubmonoid.closure (Set.range f)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
PresheafOfModules.instIsRightAdjointPushforwardCompFunctorOppositeRingCatWhiskerLeftOp : ∀ {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}
  {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R)
  {G : CategoryTheory.Functor D E} {T : CategoryTheory.Functor Eᵒᵖ RingCat} (ψ : R ⟶ G.op.comp T)
  [(PresheafOfModules.pushforward φ).IsRightAdjoint] [(PresheafOfModules.pushforward ψ).IsRightAdjoint],
  (PresheafOfModules.pushforward (CategoryTheory.CategoryStruct.comp φ (F.op.whiskerLeft ψ))).IsRightAdjoint
-- Init.Data.Array.Lemmas
/-- Variant of `any_toArray` with a side condition on `stop`.  -/
List.any_toArray' : ∀ {α : Type u_1} {p : α → Bool} {l : List α} {stop : ℕ}, stop = l.toArray.size → l.toArray.any p 0 stop = l.any p
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.sub.inj : ∀ {a b a_1 b_1 : Int.Internal.Linear.Expr}, a.sub b = a_1.sub b_1 → a = a_1 ∧ b = b_1
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.mem_center_iff : ∀ {G : Type u_1} [inst : AddGroup G] {z : G}, z ∈ AddSubgroup.center G ↔ ∀ (g : G), g + z = z + g
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.step.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] (M : Λ → Turing.TM1.Stmt Γ Λ σ) (var : σ)
  (Tape : Turing.Tape Γ), Turing.TM1.step M { l := none, var := var, Tape := Tape } = none
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddMonoid : {α : Type u_1} → [AddMonoid α] → AddMonoid αᵒᵈ
-- Mathlib.Tactic.Linarith.Datatypes
/-- `l.vars` returns the list of variables that occur in `l`.  -/
Mathlib.Tactic.Linarith.Linexp.vars : Mathlib.Tactic.Linarith.Linexp → List ℕ
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- A free group basis of a free group `G`, over the set `Generators G`.  -/
IsFreeGroup.basis : (G : Type u_1) → [inst : Group G] → [inst_1 : IsFreeGroup G] → FreeGroupBasis (IsFreeGroup.Generators G) G
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E / F` is a separable extension of exponential characteristic `q`, if `{ u_i }` is a
family of elements of `E` which is `F`-linearly independent, then `{ u_i ^ (q ^ n) }` is also
`F`-linearly independent for any natural number `n`.  -/
LinearIndependent.map_pow_expChar_pow_of_isSeparable : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q n : ℕ) [hF : ExpChar F q]
  {ι : Type u_1} {v : ι → E} [Algebra.IsSeparable F E], LinearIndependent F v → LinearIndependent F fun x => v x ^ q ^ n
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.HasSmallLocalizedHom.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {X Y : C},
  Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) → CategoryTheory.Localization.HasSmallLocalizedHom W X Y
-- Init.Data.Option.Basic
Option.sequence_some : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Applicative m] (f : m α), (some f).sequence = some <$> f
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.pred_zero : Ordinal.pred 0 = 0
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
SubAddAction.ofStabilizer.isMultiplyPretransitive_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] [AddAction.IsPretransitive G α] {n : ℕ}
  {a b : α},
  AddAction.IsMultiplyPretransitive (↥(AddAction.stabilizer G a)) (↥(SubAddAction.ofStabilizer G a)) n ↔
    AddAction.IsMultiplyPretransitive (↥(AddAction.stabilizer G b)) (↥(SubAddAction.ofStabilizer G b)) n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.cosPartialEquiv_apply : ∀ (θ : ℝ), ↑Real.cosPartialEquiv θ = Real.cos θ
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.nnnorm_def : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A]
  [inst_5 : RegularNormedAlgebra 𝕜 A] (x : Unitization 𝕜 A), ‖x‖₊ = ‖(Unitization.splitMul 𝕜 A) x‖₊
-- Mathlib.Analysis.SumOverResidueClass
Nat.residueClassesEquiv.eq_1 : ∀ (N : ℕ) [inst : NeZero N],
  N.residueClassesEquiv =
    { toFun := fun n => (↑n, n / N), invFun := fun p => p.1.val + N * p.2, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.inclusion_rfl : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (L : BooleanSubalgebra α),
  BooleanSubalgebra.inclusion ⋯ = BoundedLatticeHom.id ↥L
-- Mathlib.RingTheory.Localization.LocalizationLocalization
IsFractionRing.instAtPrimeFractionRing : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] (p : Ideal R) [inst_2 : p.IsPrime],
  IsFractionRing (Localization.AtPrime p) (FractionRing R)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.domRestrictHom.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] {S : Type u_5} [inst_1 : SetLike S M] [inst_2 : AddSubmonoidClass S M] (M' : S)
  (A : Type u_6) [inst_3 : AddCommMonoid A],
  AddMonoidHom.domRestrictHom M' A = { toFun := fun f => f.domRestrict M', map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Baire.Lemmas
/-- Baire theorem: the intersection of two dense Gδ sets is dense.  -/
Dense.inter_of_Gδ : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {s t : Set X},
  IsGδ s → IsGδ t → Dense s → Dense t → Dense (s ∩ t)
-- Mathlib.Topology.DiscreteSubset
mem_codiscrete_accPt : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set X},
  S ∈ Filter.codiscrete X ↔ ∀ (x : X), ¬AccPt x (Filter.principal Sᶜ)
-- Mathlib.Algebra.Group.Embedding
/-- If right-addition by any element is cancellative, right-addition by `g` is an embedding.  -/
addRightEmbedding : {G : Type u_1} → [inst : Add G] → [IsRightCancelAdd G] → G → G ↪ G
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the forward direction of `upperHemicontinuous_iff_forall_isOpen`. -/
UpperHemicontinuous.forall_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} [inst_1 : TopologicalSpace β],
  UpperHemicontinuous f → ∀ (x : α) (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhds x, f x' ⊆ u
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.negAt.eq_1 : ∀ {K : Type u_1} [inst : Field K] (s : Set { w // w.IsReal }),
  NumberField.mixedEmbedding.negAt s =
    (ContinuousLinearEquiv.piCongrRight fun w =>
          if w ∈ s then ContinuousLinearEquiv.neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ).prodCongr
      (ContinuousLinearEquiv.refl ℝ ({ w // w.IsComplex } → ℂ))
-- Mathlib.Order.Sublocale
Sublocale.coe_inf : ∀ {X : Type u_1} [inst : Order.Frame X] {S : Sublocale X} (a b : ↥S), ↑(a ⊓ b) = ↑a ⊓ ↑b
-- Mathlib.Order.Category.BddOrd
BddOrd.coe_comp : ∀ {X Y Z : BddOrd} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
/-- **Chevalley's Theorem**: The image of a constructible set under a
morphism of finite presentation into a qcqs scheme is constructible.  -/
AlgebraicGeometry.Scheme.Hom.isConstructible_image : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFinitePresentation f]
  [AlgebraicGeometry.QuasiCompact f] [CompactSpace ↥Y] [QuasiSeparatedSpace ↥Y] {s : Set ↥X},
  Topology.IsConstructible s → Topology.IsConstructible (⇑f '' s)
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
_private.Mathlib.MeasureTheory.Function.AEEqOfIntegral.0.MeasureTheory.«term⟪_,_⟫» : Lean.ParserDescr
-- Lean.Meta.Tactic.Cases
Lean.Meta.Cases.Context.majorTypeFn : Lean.Meta.Cases.Context → Lean.Expr
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNat.eq_1 : ∀ (n : ℕ), Turing.PartrecToTM2.trNat n = Turing.PartrecToTM2.trNum ↑n
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Ico_eq_integral_Ioo : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x y : X} [MeasureTheory.NullSingletonClass μ],
  ∫ (t : X) in Set.Ico x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compl₂_apply : ∀ {R : Type u_14} {R₂ : Type u_15} {R₃ : Type u_16} {R₄ : Type u_17} {R₅ : Type u_18} {M : Type u_19} {N : Type u_20}
  {P : Type u_21} {Q : Type u_22} [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  [inst_3 : Semiring R₄] [inst_4 : Semiring R₅] {σ₂₃ : R₂ →+* R₃} {σ₄₂ : R₄ →+* R₂} {σ₄₃ : R₄ →+* R₃}
  [inst_5 : AddCommMonoid M] [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid P] [inst_8 : AddCommMonoid Q]
  [inst_9 : Module R M] [inst_10 : Module R₂ N] [inst_11 : Module R₃ P] [inst_12 : Module R₄ Q] [inst_13 : Module R₅ P]
  [inst_14 : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃] [inst_15 : SMulCommClass R₃ R₅ P] {σ₁₅ : R →+* R₅}
  (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) (g : Q →ₛₗ[σ₄₂] N) (m : M) (q : Q), ((h.compl₂ g) m) q = (h m) (g q)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_le_size_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)}, t.size - 1 ≤ (t.alter k f).size
-- Mathlib.Logic.Encodable.Basic
ULower.ext : ∀ {α : Type u_1} [inst : Encodable α] {a b : ULower α}, a.up = b.up → a = b
-- Mathlib.CategoryTheory.Category.Preorder
/-- Construct a morphism in the opposite of a preorder category from an inequality.  -/
CategoryTheory.opHomOfLE : {X : Type u} → [inst : Preorder X] → {x y : Xᵒᵖ} → Opposite.unop x ≤ Opposite.unop y → (y ⟶ x)
-- Mathlib.Order.RelClasses
instIsLinearOrderLe : ∀ {α : Type u} [inst : LinearOrder α], IsLinearOrder α fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.instAddLeftMono : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α], AddLeftMono (Finset α)
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E` is an algebraic closure of `F`, then `F` is perfect if and only if `E / F` is
separable.  -/
perfectField_iff_isSeparable_algebraicClosure : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsAlgClosure F E],
  PerfectField F ↔ Algebra.IsSeparable F E
-- Std.Internal.Do.WP.Conjunctive
/-- `Option` is conjunctive: its `wp` is evaluation at the result.  -/
Std.Internal.Do.Option.instWPConjunctive : ∀ {α : Type u}, Std.Internal.Do.WPConjunctive (Option α) α Prop Prop
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- The second projection from the mapping cone, as a cochain of degree `0`.  -/
CochainComplex.mappingCone.snd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ : F ⟶ G) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            CochainComplex.HomComplex.Cochain (CochainComplex.mappingCone φ) G 0
-- Mathlib.RingTheory.Coalgebra.Convolution
LinearMap.convOne_def : ∀ {R : Type u_1} {A : Type u_3} {C : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid C] [inst_4 : Module R C] [inst_5 : Coalgebra R C],
  1 = WithConv.toConv (Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.map_comp_id : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {C : Type uC} {E : Type uE} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Algebra S C]
  [inst_10 : IsScalarTower R S C] [inst_11 : Semiring E] [inst_12 : Algebra R E] [inst_13 : Algebra S E]
  [inst_14 : IsScalarTower R S E] (f₂ : C →ₐ[S] E) (f₁ : A →ₐ[S] C),
  Algebra.TensorProduct.map (f₂.comp f₁) (AlgHom.id R E) =
    (Algebra.TensorProduct.map f₂ (AlgHom.id R E)).comp (Algebra.TensorProduct.map f₁ (AlgHom.id R E))
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModuleHierarchyImportsParams.module : Lean.Lsp.LeanModuleHierarchyImportsParams → Lean.Lsp.LeanModule
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.HasHomotopyCofiber.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} {φ : F ⟶ G},
  (∀ (i j : ι), c.Rel i j → CategoryTheory.Limits.HasBinaryBiproduct (F.X j) (G.X i)) →
    HomologicalComplex.HasHomotopyCofiber φ
-- Mathlib.Dynamics.OmegaLimit
omegaLimit.eq_1 : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α),
  omegaLimit f ϕ s = ⋂ u ∈ f, closure (Set.image2 ϕ u s)
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.autMulEquivAutGalois.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.PreGaloisCategory.autMulEquivAutGalois F = CategoryTheory.PreGaloisCategory.autMulEquivAutGalois F
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.instIsCentralScalar : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {S : Type u_10} [inst_5 : Monoid S]
  [inst_6 : DistribMulAction S N] [inst_7 : SMulCommClass R S N] [inst_8 : DistribMulAction Sᵐᵒᵖ N]
  [inst_9 : IsCentralScalar S N], IsCentralScalar S (M [⋀^ι]→ₗ[R] N)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullback_snd_iso_of_left_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f], CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
Continuous.integrableOn_uIcc : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} {a b : X}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [inst_5 : LinearOrder X] [CompactIccSpace X] [T2Space X],
  Continuous f → MeasureTheory.IntegrableOn f (Set.uIcc a b) μ
-- Batteries.Data.List.Basic
List.fillNones.eq_def : ∀ {α : Type u_1} (x : List (Option α)) (x_1 : List α),
  x.fillNones x_1 =
    match x, x_1 with
    | [], x => []
    | some a :: as, as' => a :: as.fillNones as'
    | none :: as, [] => as.reduceOption
    | none :: as, a :: as' => a :: as.fillNones as'
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.instFinite : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [Std.Iterators.Productive α m], Std.Iterators.Finite (Std.Iterators.Types.Take α m) m
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
RingHom.IsIntegral.trans : ∀ {R : Type u_1} {S : Type u_4} {T : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  (f : R →+* S) (g : S →+* T), f.IsIntegral → g.IsIntegral → (g.comp f).IsIntegral
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.coconeOfCoconeUncurry_pt : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} {D : CategoryTheory.Limits.DiagramOfCocones F}
  (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j))
  (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.uncurry.obj F)),
  (CategoryTheory.Limits.coconeOfCoconeUncurry Q c).pt = c.pt
-- Mathlib.Probability.Moments.SubGaussian
/-- For `X, Y` two independent sub-Gaussian random variables such that `μ[X] ≥ μ[Y]`,
the probability that `X ≤ Y` is bounded by an exponential decay term.  -/
ProbabilityTheory.HasSubgaussianMGF.measureReal_le_le_exp : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} {cX cY : NNReal},
  ProbabilityTheory.HasSubgaussianMGF (fun ω => X ω - ∫ (x : Ω), X x ∂μ) cX μ →
    ProbabilityTheory.HasSubgaussianMGF (fun ω => Y ω - ∫ (x : Ω), Y x ∂μ) cY μ →
      ProbabilityTheory.IndepFun X Y μ →
        ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ →
          μ.real {ω | X ω ≤ Y ω} ≤ Real.exp (-(∫ (x : Ω), Y x ∂μ - ∫ (x : Ω), X x ∂μ) ^ 2 / (2 * (↑cX + ↑cY)))
-- Mathlib.Analysis.Normed.Group.BallSphere
instContinuousNegElemClosedBallOfNat : ∀ {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ}, ContinuousNeg ↑(Metric.closedBall 0 r)
-- Lean.Meta.DiscrTree.Types
/-- Discrimination tree key. See `DiscrTree`
 -/
Lean.Meta.DiscrTree.Key : Type
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientWithinAt.differentiableWithinAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F},
  HasGradientWithinAt f f' s x → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_left_monotone : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] {a : M}, 0 ≤ a → Monotone fun n => n • a
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorems.mk.sizeOf_spec : ∀ (lemmas : Lean.SMap Lean.Name (List Lean.Meta.SimpCongrTheorem)), sizeOf { lemmas := lemmas } = 1 + sizeOf lemmas