mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.pushforwardId_hom_counit_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : C)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id I)]
  [inst_2 : CategoryTheory.ExponentiableMorphism (CategoryTheory.CategoryStruct.id I)]
  {Z : CategoryTheory.Functor (CategoryTheory.Over I) (CategoryTheory.Over I)}
  (h : CategoryTheory.Functor.id (CategoryTheory.Over I) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.ExponentiableMorphism.pushforwardId I).hom
        (CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.CategoryStruct.id I)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.id I)).counit h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.id I)).counit h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getEntryLT?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryLT? k = t₂.getEntryLT? k
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.functorMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY))
      C]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)]
  [inst_4 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πY)
      (CategoryTheory.SmallObject.functorObjLeft f πY)],
  CategoryTheory.SmallObject.functorMap f τ =
    CategoryTheory.Limits.pushout.map (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX) (CategoryTheory.SmallObject.functorObjTop f πY)
      (CategoryTheory.SmallObject.functorObjLeft f πY) (CategoryTheory.Arrow.Hom.left τ)
      (CategoryTheory.SmallObject.functorMapTgt f τ) (CategoryTheory.SmallObject.functorMapSrc f τ) ⋯ ⋯
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.unoneD_coe : ∀ {α : Type u} (d x : α), WithOne.unoneD d ↑x = x
-- Init.Data.Array.Lex.Lemmas
Array.lex_toList : ∀ {α : Type u_1} [inst : BEq α] {lt : α → α → Bool} {xs ys : Array α}, xs.toList.lex ys.toList lt = xs.lex ys lt
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomInvPair.mk : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ : R₁ →+* R₂}
  {σ' : outParam (R₂ →+* R₁)}, σ'.comp σ = RingHom.id R₁ → σ.comp σ' = RingHom.id R₂ → RingHomInvPair σ σ'
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.ShouldCanonResult.canonImplicit : Lean.Meta.Sym.Canon.ShouldCanonResult✝
-- Mathlib.Algebra.Order.UpperLower
upperClosure_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α], upperClosure 0 = 0
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceLT : Lean.Meta.Simp.Simproc
-- Mathlib.Data.List.Permutation
List.permutationsAux2_snd_cons : ∀ {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (y : α) (ys : List α) (f : List α → β),
  (List.permutationsAux2 t ts r (y :: ys) f).2 =
    f (t :: y :: ys ++ ts) :: (List.permutationsAux2 t ts r ys fun x => f (y :: x)).2
-- Mathlib.Order.Basic
/-- A subtype of a linear order is a linear order. We explicitly give the proofs of decidable
equality and decidable order in order to ensure the decidability instances are all definitionally
equal.  -/
Subtype.instLinearOrder : {α : Type u_2} → [LinearOrder α] → (p : α → Prop) → LinearOrder (Subtype p)
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sum_Ioc_mul_eq_sum_sum : ∀ {R : Type u_2} [inst : Semiring R] (f g : ArithmeticFunction R) (N : ℕ),
  ∑ n ∈ Finset.Ioc 0 N, (f * g) n = ∑ n ∈ Finset.Ioc 0 N, f n * ∑ m ∈ Finset.Ioc 0 (N / n), g m
-- Mathlib.NumberTheory.Modular
/-- The standard (closed) fundamental domain of the action of `SL(2,ℤ)` on `ℍ`.  -/
Modular.term𝒟 : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffOn_fst : ∀ {𝕜 : 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] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {G : Type u_9} [inst_8 : TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {s : Set (M × N)},
  ContMDiffOn (I.prod J) I n Prod.fst s
-- Mathlib.Data.Num.Bitwise
SNum.zero : Bool → SNum
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mul_eq_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α}, s * t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.constantsToVars.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} (x : (L.withConstants γ).Term α),
  x.constantsToVars =
    match x with
    | FirstOrder.Language.var a => FirstOrder.Language.var (Sum.inr a)
    | FirstOrder.Language.func f ts =>
      Sum.casesOn f (fun f => FirstOrder.Language.func f fun i => (ts i).constantsToVars) fun c =>
        FirstOrder.Language.var (Sum.inl c)
    | FirstOrder.Language.func f ts =>
      Sum.casesOn f (fun f => FirstOrder.Language.func f fun i => (ts i).constantsToVars) fun c => isEmptyElim c
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity follows from scaled non-negative distance. Backward direction of
`similar_iff_exists_nndist_eq`.  -/
Similar.of_exists_nndist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  (∃ r, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)) → Similar v₁ v₂
-- Mathlib.GroupTheory.OreLocalization.Basic
_private.Mathlib.GroupTheory.OreLocalization.Basic.0.AddOreLocalization.vadd''.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] (r : R) (s : ↥S),
  AddOreLocalization.vadd''✝ r s = AddOreLocalization.liftExpand (AddOreLocalization.vadd'✝ r s) ⋯
-- Lean.Data.Lsp.Extra
/-- The goals as pretty-printed Markdown, or something like "no goals" if accomplished.  -/
Lean.Lsp.PlainGoal.rendered : Lean.Lsp.PlainGoal → String
-- ProofWidgets.Component.MakeEditLink
/-- Which textual range to select after the edit.
The range is interpreted in the file that `edit` applies to.
If present and `start == end`, the cursor is moved to `start` and nothing is selected.
If not present, the selection is not changed.  -/
ProofWidgets.MakeEditLinkProps.newSelection? : ProofWidgets.MakeEditLinkProps → Option Lean.Lsp.Range
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev_eq_iff : ∀ {s : String.Slice} {p q : s.Pos} {h : p ≠ s.startPos}, p.prev h = q ↔ q < p ∧ ∀ q' < p, q' ≤ q
-- Mathlib.RingTheory.Adjoin.FG
Subalgebra.fg_bot : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], ⊥.FG
-- Mathlib.FieldTheory.RatFunc.Degree
RatFunc.intDegree_mul : ∀ {K : Type u} [inst : Field K] {x y : RatFunc K}, x ≠ 0 → y ≠ 0 → (x * y).intDegree = x.intDegree + y.intDegree
-- Mathlib.Algebra.Category.Grp.Zero
GrpCat.isZero_of_iff_subsingleton : ∀ {G : Type u_1} [inst : Group G], CategoryTheory.Limits.IsZero (GrpCat.of G) ↔ Subsingleton G
-- Mathlib.CategoryTheory.Types.Basic
/-- The sections of a functor `F : J ⥤ Type` are
the choices of a point `u j : F.obj j` for each `j`,
such that `F.map f (u j) = u j'` for every morphism `f : j ⟶ j'`.

We later use these to define limits in `Type` and in many concrete categories.
 -/
CategoryTheory.Functor.sections : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] → (F : CategoryTheory.Functor J (Type w)) → Set ((j : J) → F.obj j)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.mk_intCast : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (n : ℤ),
  ArchimedeanClass.FiniteElement.mk ↑n ⋯ = ↑n
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_rightUnitor_hom : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {L : CategoryTheory.Functor A B} {R : CategoryTheory.Functor B A} (adj : L ⊣ R),
  (CategoryTheory.conjugateEquiv adj (adj.comp CategoryTheory.Adjunction.id)) L.rightUnitor.hom = R.leftUnitor.inv
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
/-- the morphism to the single chain complex with `Z` in degree `0` is a quasi-isomorphism  -/
CategoryTheory.ProjectiveResolution.quasiIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.ProjectiveResolution Z),
  QuasiIso self.π
-- Mathlib.Data.Set.Opposite
Set.singleton_op_unop : ∀ {α : Type u_1} (x : α), {Opposite.op x}.unop = {x}
-- Mathlib.Algebra.Order.Monoid.Defs
/-- An ordered (additive) monoid is a monoid with a preorder such that addition is monotone.  -/
IsOrderedAddMonoid : (α : Type u_2) → [AddCommMonoid α] → [Preorder α] → Prop
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- `CondensedSet.LocallyConstant.functor` is isomorphic to `Condensed.discrete`
(by uniqueness of adjoints).
 -/
CondensedSet.LocallyConstant.iso : CondensedSet.LocallyConstant.functor ≅ Condensed.discrete (Type (u + 1))
-- Mathlib.RingTheory.Polynomial.HilbertPoly
_private.Mathlib.RingTheory.Polynomial.HilbertPoly.0.Polynomial.hilbertPoly.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (d : ℕ) (h_1 : Unit → motive 0) (h_2 : (d : ℕ) → motive d.succ),
  (match d.succ with
    | 0 => h_1 ()
    | d.succ => h_2 d) =
    h_2 d
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_midpoint_right : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V]
  [inst_5 : Invertible 2] (p₁ p₂ : P), dist (midpoint 𝕜 p₁ p₂) p₂ = ‖2‖⁻¹ * dist p₁ p₂
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mulVec_injective_of_invertible : ∀ {m : Type u} [inst : DecidableEq m] {K : Type u_3} [inst_1 : Field K] [inst_2 : Fintype m] (A : Matrix m m K)
  [Invertible A], Function.Injective A.mulVec
-- Init.System.IO
/-- Creates a temporary directory in the most secure manner possible, providing its path to an `IO`
action. Afterwards, all files in the temporary directory are recursively deleted, regardless of how
or when they were created.

There are no race conditions in the directory’s creation. The directory is readable and writable
only by the creating user ID. Use `IO.FS.createTempDir` to avoid the automatic deletion of the
directory's contents.
 -/
IO.FS.withTempDir : {m : Type → Type u_1} → {α : Type} → [Monad m] → [MonadFinally m] → [MonadLiftT IO m] → (System.FilePath → m α) → m α
-- Mathlib.LinearAlgebra.InvariantBasisNumber
/-- Any nontrivial ring satisfying Orzech property also satisfies strong rank condition.  -/
strongRankCondition_of_orzechProperty : ∀ (R : Type u) [inst : Semiring R] [Nontrivial R] [OrzechProperty R], StrongRankCondition R
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.insertListIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)), Std.Internal.List.insertListIfNew l [] = l
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E / F` is a separable field extension of exponential characteristic `q`, then
`F(S) = F(S ^ (q ^ n))` for any subset `S` of `E` and any natural number `n`.  -/
IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable' : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsSeparable F E]
  (S : Set E) (q : ℕ) [ExpChar F q] (n : ℕ),
  IntermediateField.adjoin F S = IntermediateField.adjoin F ((fun x => x ^ q ^ n) '' S)
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars.eq_1 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R), p.vars = p.degrees.toFinset
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.ωSup_apply_ωSup : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (c₀ : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (c₁ : OmegaCompletePartialOrder.Chain α),
  (OmegaCompletePartialOrder.ωSup c₀) (OmegaCompletePartialOrder.ωSup c₁) =
    OmegaCompletePartialOrder.ContinuousHom.Prod.apply (OmegaCompletePartialOrder.ωSup (c₀.zip c₁))
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- Angles in a vector space are invariant under inversion.  -/
EuclideanGeometry.angle_const_sub : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (v v₁ v₂ v₃ : V),
  EuclideanGeometry.angle (v - v₁) (v - v₂) (v - v₃) = EuclideanGeometry.angle v₁ v₂ v₃
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.mass.eq_1 : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω), μ.mass = μ Set.univ
-- Mathlib.Algebra.CharP.Lemmas
add_pow_eq_mul_pow_add_pow_div_char_of_commute : ∀ {R : Type u_1} [inst : Semiring R] {x y : R} (p n : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p],
  Commute x y → (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In a preadditive category, any finite bicone which is a limit cone is in fact a bilimit
bicone.  -/
CategoryTheory.Limits.isBilimitOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {J : Type u_1} →
        [Fintype J] →
          {f : J → C} → (t : CategoryTheory.Limits.Bicone f) → CategoryTheory.Limits.IsLimit t.toCone → t.IsBilimit
-- Init.Data.Array.Lemmas
/-- Variant of `any_append` with a side condition for the `stop` argument.  -/
Array.any_append' : ∀ {α : Type u_1} {stop : ℕ} {f : α → Bool} {xs ys : Array α},
  stop = (xs ++ ys).size → (xs ++ ys).any f 0 stop = (xs.any f || ys.any f)
-- Mathlib.Topology.MetricSpace.Congruence
/-- Congruence follows from pairwise preserved extended distance. Backward direction of
`congruent_iff_pairwise_edist_eq`.  -/
Congruent.of_pairwise_edist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂],
  (Pairwise fun i₁ i₂ => edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)) → Congruent v₁ v₂
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nontrivial.add : ∀ {α : Type u_2} [inst : Add α] [IsLeftCancelAdd α] {s t : Set α}, s.Nontrivial → t.Nontrivial → (s + t).Nontrivial
-- Mathlib.Data.Int.NatAbs
/-- `Int.natAbs` as a bundled `MonoidWithZeroHom`.  -/
Int.natAbsHom : ℤ →*₀ ℕ
-- Mathlib.RingTheory.FreeCommRing
FreeRing.coe_zero : ∀ (α : Type u), ↑0 = 0
-- Mathlib.Analysis.Normed.Group.Constructions
PUnit.normedAddCommGroup : NormedAddCommGroup PUnit.{u_5 + 1}
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.range_evalᵢ : ∀ (σ K : Type u) [inst : Fintype K] [inst_1 : Field K] [Finite σ], (MvPolynomial.evalᵢ σ K).range = ⊤
-- Mathlib.Order.Category.Semilat
SemilatInfCat.of.injEq : ∀ (X : Type u) [isSemilatticeInf : SemilatticeInf X] [isOrderTop : OrderTop X] (X_1 : Type u)
  (isSemilatticeInf_1 : SemilatticeInf X_1) (isOrderTop_1 : OrderTop X_1),
  ({ X := X, isSemilatticeInf := isSemilatticeInf, isOrderTop := isOrderTop } =
      { X := X_1, isSemilatticeInf := isSemilatticeInf_1, isOrderTop := isOrderTop_1 }) =
    (X = X_1 ∧ isSemilatticeInf ≍ isSemilatticeInf_1 ∧ isOrderTop ≍ isOrderTop_1)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.conjTranspose_kroneckerTMul : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α]
  [inst_4 : Module R β] [inst_5 : StarRing R] [inst_6 : StarAddMonoid α] [inst_7 : StarAddMonoid β]
  [inst_8 : StarModule R α] [inst_9 : StarModule R β] (x : Matrix l m α) (y : Matrix n p β),
  (Matrix.kroneckerMap (TensorProduct.tmul R) x y).conjTranspose =
    Matrix.kroneckerMap (TensorProduct.tmul R) x.conjTranspose y.conjTranspose
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- `LinearIndependent R v` states the family of vectors `v` is linearly independent over `R`.  -/
LinearIndependent : {ι : Type u'} →
  (R : Type u_2) → {M : Type u_4} → (ι → M) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
-- Mathlib.Analysis.Convex.Topology
/-- If `x ∈ s` and `y ∈ interior s`, then the segment `(x, y]` is included in `interior s`.  -/
Convex.add_smul_sub_mem_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
  [AddRightMono 𝕜] {s : Set E},
  Convex 𝕜 s → ∀ {x y : E}, x ∈ s → y ∈ interior s → ∀ {t : 𝕜}, t ∈ Set.Ioc 0 1 → x + t • (y - x) ∈ interior s
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- The generating equivalence relation for elements of the power algebra
that are identified in the free product  -/
LinearAlgebra.FreeProduct.rel' : {I : Type u} →
  [DecidableEq I] →
    (R : Type v) →
      [inst : CommSemiring R] →
        (A : I → Type w) →
          [inst_1 : (i : I) → Semiring (A i)] →
            [inst_2 : (i : I) → Algebra R (A i)] →
              (DirectSum ℕ fun n => TensorPower R n (DirectSum I fun i => A i)) →
                (DirectSum ℕ fun n => TensorPower R n (DirectSum I fun i => A i)) → Prop
-- Mathlib.Data.Vector3
_private.Mathlib.Data.Vector3.0.Fin2.add.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match k.succ with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_2 k
-- Mathlib.Order.SuccPred.Basic
Order.Ioi_pred_eq_insert : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a : α),
  Set.Ioi (Order.pred a) = insert a (Set.Ioi a)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- If the addition is `C^n`, then it is continuous. This is not an instance for
technical reasons, see note [Design choices about smooth algebraic structures].  -/
continuousAdd_of_contMDiffAdd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  {G : Type u_4} [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G],
  ContinuousAdd G
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- The 2-cells between a parallel pair of 1-cells `f g` in `CatEnrichedOrdinary C` are defined to
be the morphisms in the hom-categories provided by the `EnrichedCategory Cat C` structure between
the corresponding objects.  -/
CategoryTheory.CatEnrichedOrdinary.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] →
      {X Y : CategoryTheory.CatEnrichedOrdinary C} → (X ⟶ Y) → (X ⟶ Y) → Type v'
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mul_nc : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.evaluation_naturality_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {V : Y.Opens} (x : ↥X) (hx : f x ∈ V) {Z : CommRingCat}
  (h : X.residueField x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.evaluation V (f x) hx)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f V)
      (CategoryTheory.CategoryStruct.comp (X.evaluation ((TopologicalSpace.Opens.map f.base).obj V) x hx) h)
-- Batteries.Data.List.Interleave
List.interleave_append_right : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁.length ≤ l₂.length + 1 → ∀ (l₃ : List α), l₁.interleave (l₂ ++ l₃) = l₁.interleave l₂ ++ l₃
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α},
  k ∉ m → l.contains k = false → (m.insertManyIfNewUnit l).getKey? k = none
-- Mathlib.RingTheory.Invariant.Basic
MulSemiringAction.smul_charpoly : ∀ {B : Type u_2} {G : Type u_3} [inst : CommRing B] [inst_1 : Group G] [inst_2 : MulSemiringAction G B]
  [inst_3 : Fintype G] (b : B) (g : G), g • MulSemiringAction.charpoly G b = MulSemiringAction.charpoly G b
-- Mathlib.Data.Nat.ChineseRemainder
Nat.chineseRemainderOfList.eq_2 : ∀ {ι : Type u_1} (a s : ι → ℕ) (i : ι) (l : List ι) (co : List.Pairwise (Function.onFun Nat.Coprime s) (i :: l)),
  Nat.chineseRemainderOfList a s (i :: l) co =
    ⟨↑(Nat.chineseRemainder ⋯ (a i) ↑(Nat.chineseRemainderOfList a s l ⋯)), ⋯⟩
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.laplacianCLM_eq : ∀ (𝕜 : Type u_2) {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace ℝ F] [inst_3 : InnerProductSpace ℝ E] [inst_4 : FiniteDimensional ℝ E] [inst_5 : RCLike 𝕜]
  [inst_6 : NormedSpace 𝕜 F] (f : SchwartzMap E F),
  (LineDeriv.laplacianCLM 𝕜 E (SchwartzMap E F)) f = Laplacian.laplacian f
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.Transcendental.infinite : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Nontrivial R]
  [Algebra.Transcendental R A], Infinite A
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
intervalIntegral.mul_integral_comp_add_mul : ∀ {a b : ℝ} {f : ℝ → ℝ} (c d : ℝ), c * ∫ (x : ℝ) in a..b, f (d + c * x) = ∫ (x : ℝ) in d + c * a..d + c * b, f x
-- Mathlib.RingTheory.Polynomial.Wronskian
/-- Wronskian of a pair of polynomials, `W(a, b) = ab' - a'b`.  -/
Polynomial.wronskian : {R : Type u_1} → [inst : CommRing R] → Polynomial R → Polynomial R → Polynomial R
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.coeFnAddMonoidHom_apply : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (D : LieDerivation R L M), LieDerivation.coeFnAddMonoidHom D = ⇑D
-- Batteries.Util.Cache
Batteries.Tactic.instNonemptyDeclCache : ∀ {α : Type} [Nonempty α], Nonempty (Batteries.Tactic.DeclCache α)
-- Lean.Environment
Lean.instReprOLeanLevel.repr : Lean.OLeanLevel → ℕ → Std.Format
-- Init.Tactics
/-- `decide_cbv` is a finishing tactic that closes goals of the form `p`, where `p`
is a `Decidable` proposition. It proceeds in two steps:
1. Apply `of_decide_eq_true` to transform the goal into `decide p = true`.
2. Reduce `decide p` via call-by-value normalization. If the result is
   definitionally equal to `true`, the goal is closed.

`decide_cbv` fails with an error if `decide p` does not reduce to `true`.
Unlike `cbv`, `decide_cbv` is a terminal tactic: it either closes the goal or
fails.

The proofs produced by `decide_cbv` only use the three standard axioms.
In particular, they do not require trust in the correctness of the code
generator.
 -/
Lean.Parser.Tactic.decide_cbv : Lean.ParserDescr