mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- The codomain of an equivariant map of large image is preprimitive if the domain is.  -/
MulAction.IsPreprimitive.of_card_lt : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] {H : Type u_3} {Y : Type u_4}
  [inst_2 : Group H] [inst_3 : MulAction H Y] {φ : G → H} {f : X →ₑ[φ] Y} [Finite Y] [MulAction.IsPretransitive H Y]
  [MulAction.IsPreprimitive G X], Nat.card Y < 2 * (Set.range ⇑f).ncard → MulAction.IsPreprimitive H Y
-- Mathlib.Order.Minimal
minimal_mem_Ico : ∀ {α : Type u_2} {x : α} [inst : PartialOrder α] {a b : α}, a < b → (Minimal (fun x => x ∈ Set.Ico a b) x ↔ x = a)
-- Mathlib.Algebra.Group.Defs
sub_self : ∀ {G : Type u_1} [inst : AddGroup G] (a : G), a - a = 0
-- Std.Data.DTreeMap.Raw.Basic
/-- Internal implementation detail of the tree map.  -/
Std.DTreeMap.Raw.inner : {α : Type u} →
  {β : α → Type v} →
    {_cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw._auto_1} →
      Std.DTreeMap.Raw α β _cmp → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.drop.eq_2 : ∀ {α : Type u} (s : Stream'.WSeq α) (n : ℕ), s.drop n.succ = (s.drop n).tail
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_of_mem_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t.keys → k ∈ t
-- Init.Data.SInt.Lemmas
ISize.mul_sub : ∀ {a b c : ISize}, a * (b - c) = a * b - a * c
-- Mathlib.Algebra.Group.Units.Opposite
isAddUnit_unop : ∀ {M : Type u_2} [inst : AddMonoid M] {m : Mᵃᵒᵖ}, IsAddUnit (AddOpposite.unop m) ↔ IsAddUnit m
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Bundle.ContMDiffRiemannianMetric.contMDiff : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  [inst_3 : TopologicalSpace B] [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℝ F] {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_8 : (b : B) → TopologicalSpace (E b)] [inst_9 : (b : B) → AddCommGroup (E b)]
  [inst_10 : (b : B) → Module ℝ (E b)] [inst_11 : FiberBundle F E] [inst_12 : VectorBundle ℝ F E]
  (self : Bundle.ContMDiffRiemannianMetric IB n F E),
  ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n fun b => ⟨b, self.inner b⟩
-- Mathlib.Algebra.Field.Basic
Commute.div_sub_div : ∀ {K : Type u_1} [inst : DivisionRing K] {a b c d : K},
  Commute b c → Commute b d → b ≠ 0 → d ≠ 0 → a / b - c / d = (a * d - b * c) / (b * d)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (hlb : l.Balanced)
  (hrb : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size),
  Std.DTreeMap.Internal.Impl.balanceL k v l r hlb hrb hlr =
    match r, hrb, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hrb, hlr =>
      match l, hlb, hlr with
      | Std.DTreeMap.Internal.Impl.leaf, hlb, hlr =>
        Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf
      | Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
        hlb, hlr => Std.DTreeMap.Internal.Impl.inner 2 k v l Std.DTreeMap.Internal.Impl.leaf
      |
      Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
          (Std.DTreeMap.Internal.Impl.inner size_1 lrk lrv l r),
        hlb, hlr =>
        Std.DTreeMap.Internal.Impl.inner 3 lrk lrv
          (Std.DTreeMap.Internal.Impl.inner 1 lk lv Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
          (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
      |
      Std.DTreeMap.Internal.Impl.inner size lk lv (ll@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r))
          Std.DTreeMap.Internal.Impl.leaf,
        hlb, hlr =>
        Std.DTreeMap.Internal.Impl.inner 3 lk lv ll
          (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
      |
      Std.DTreeMap.Internal.Impl.inner ls lk lv (Std.DTreeMap.Internal.Impl.inner lls k v l r)
          (Std.DTreeMap.Internal.Impl.inner lrs k_1 v_1 l_1 r_1),
        hlb, hlr => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l_1 r_1, hrb, hlr =>
      match l, hlb, hlr with
      | Std.DTreeMap.Internal.Impl.leaf, hlb, hlr =>
        Std.DTreeMap.Internal.Impl.inner (1 + rs) k v Std.DTreeMap.Internal.Impl.leaf r
      | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr, hlb, hlr =>
        if hlsd : Std.DTreeMap.Internal.delta * rs < ls then
          match ll, lr, hlb, hlr with
          | Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l r_2, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr,
            hlb, hlr =>
            if lrs < Std.DTreeMap.Internal.ratio * lls then
              Std.DTreeMap.Internal.Impl.inner (1 + ls + rs) lk lv ll
                (Std.DTreeMap.Internal.Impl.inner (1 + rs + lrs) k v
                  (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr) r)
            else
              Std.DTreeMap.Internal.Impl.inner (1 + ls + rs) lrk lrv
                (Std.DTreeMap.Internal.Impl.inner (1 + lls + lrl.size) lk lv ll lrl)
                (Std.DTreeMap.Internal.Impl.inner (1 + rs + lrr.size) k v lrr r)
          | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf, hlb, hlr => ⋯.elim
          | Std.DTreeMap.Internal.Impl.leaf, x, hlb, hlr => ⋯.elim
        else Std.DTreeMap.Internal.Impl.inner (1 + ls + rs) k v (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) r
-- Init.Data.Vector.Lemmas
Vector.getElem_drop : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n} {j : ℕ} (hi : i < n - j), (xs.drop j)[i] = xs[j + i]
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∈ t₂ → (t₁ \ t₂).getD k fallback = fallback
-- Mathlib.Lean.MessageData.ForExprs
Lean.MessageData.Exprs.mk.sizeOf_spec : ∀ (msg : Lean.MessageData), sizeOf { msg := msg } = 1 + sizeOf msg
-- Aesop.Builder.Basic
Aesop.RuleBuilderOptions.pattern? : Aesop.RuleBuilderOptions → Option Lean.Term
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
/-- The symplectic complement of a closed submodule with respect to `⟪⬝, ⬝⟫.im`, defined as the
image of `mulI` and `orthogonal`. The proof that this is the symplectic complement is given by
`mem_symplComp_iff`.  -/
ClosedSubmodule.symplComp : {H : Type u_1} →
  [inst : NormedAddCommGroup H] → [ipc : InnerProductSpace ℂ H] → ClosedSubmodule ℝ H → ClosedSubmodule ℝ H
-- Mathlib.Logic.Equiv.Option
Equiv.optionSubtype.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (x : β),
  Equiv.optionSubtype x =
    {
      toFun := fun e =>
        { toFun := fun a => ⟨↑e (some a), ⋯⟩, invFun := fun b => ((↑e).symm ↑b).get ⋯, left_inv := ⋯, right_inv := ⋯ },
      invFun := fun e =>
        ⟨{ toFun := fun a => a.casesOn' x (Subtype.val ∘ ⇑e),
            invFun := fun b => if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
          ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.weightSpace_le_genWeightSpace : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [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]
  [inst_7 : LieRing.IsNilpotent L] (χ : L → R), LieModule.weightSpace M χ ≤ LieModule.genWeightSpace M χ
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
HomogeneousLocalization.localRingHom.congr_simp : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {B : Type u_4} {τ : Type u_5} [inst_6 : CommRing B] [inst_7 : SetLike τ B]
  [inst_8 : AddSubgroupClass τ B] {ℬ : ι → τ} [inst_9 : GradedRing ℬ] (f f_1 : 𝒜 →+*ᵍ ℬ) (e_f : f = f_1) (I : Ideal A)
  [inst_10 : I.IsPrime] (J : Ideal B) [inst_11 : J.IsPrime] (hIJ : I = Ideal.comap f J),
  HomogeneousLocalization.localRingHom f I J hIJ = HomogeneousLocalization.localRingHom f_1 I J ⋯
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- The functions `r i` approximate the values `b i * n`.  -/
AkraBazziRecurrence.dist_r_b : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
  (self : AkraBazziRecurrence T g a b r) (i : α),
  (fun n => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun n => ↑n / Real.log ↑n ^ 2
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterMatrix.instGroupGroup : {B : Type u_1} → (M : CoxeterMatrix B) → Group M.Group
-- Mathlib.Tactic.ITauto
/-- `(p: A) ⊢ A ∨ B`  -/
Mathlib.Tactic.ITauto.Proof.orInL : Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
_private.Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic.0.ProfiniteAddGrp.Hom.mk : {A B : ProfiniteAddGrp.{u}} → (↑A.toProfinite.toTop →ₜ+ ↑B.toProfinite.toTop) → A.Hom B
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.map_comp_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* S) (g : σ → τ),
  (MvPolynomial.map f).comp (MvPolynomial.rename g).toRingHom = (MvPolynomial.rename g).comp (MvPolynomial.map f)
-- Init.Data.Nat.Lcm
Nat.lcm_mul_left_right_eq_mul_of_lcm_eq_mul : ∀ {n m k : ℕ}, n.lcm m = n * m → n.lcm (k * m) = n.lcm k * m
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_measure_zero_of_pos : ∀ {α : Type u_1} {q : ℝ} {ε : Type u_7} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε]
  [inst_2 : MeasurableSpace α] {f : α → ε}, 0 < q → MeasureTheory.eLpNorm' f q 0 = 0
-- Mathlib.Data.Vector.Defs
/-- Drop `i` elements from a vector of length `n`; we can have `i > n`.  -/
List.Vector.drop : {α : Type u_1} → {n : ℕ} → (i : ℕ) → List.Vector α n → List.Vector α (n - i)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.FullyFaithful.mapCommGrp_preimage : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F : CategoryTheory.Functor C D} [inst_6 : F.Braided] (hF : F.FullyFaithful) {X Y : CategoryTheory.CommGrp C}
  (f : F.mapCommGrp.obj X ⟶ F.mapCommGrp.obj Y),
  hF.mapCommGrp.preimage f =
    CategoryTheory.InducedCategory.homMk (CategoryTheory.Grp.homMk' (hF.mapMon.preimage f.hom.hom))
-- Mathlib.Control.Monad.Writer
WriterT.instMonadLiftOfMonoid : {M : Type u → Type v} → {ω : Type u} → [Monad M] → [Monoid ω] → MonadLift M (WriterT ω M)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_eq_bot_of_nilpotencyClass_le : ∀ {G : Type u_1} [inst : AddGroup G] {S : AddSubgroup G} [AddGroup.IsNilpotent ↥S] {n : ℕ},
  AddGroup.nilpotencyClass ↥S ≤ n → S.lowerCentralSeries n = ⊥
-- Lean.Parser.Extension
Lean.Parser.getTokenTable : Lean.Environment → Lean.Parser.TokenTable
-- Mathlib.RingTheory.Ideal.Maps
RingHom.liftOfRightInverseAux.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Ring A] [inst_1 : Ring B] [inst_2 : Ring C] (f : A →+* B)
  (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →+* C) (hg : RingHom.ker f ≤ RingHom.ker g),
  f.liftOfRightInverseAux f_inv hf g hg =
    { toFun := fun b => g (f_inv b), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Data.List.MinMax
List.argmax_eq_some_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] {f : α → β} {l : List α} {m : α} [inst_1 : DecidableEq α],
  List.argmax f l = some m ↔ m ∈ l ∧ (∀ a ∈ l, f a ≤ f m) ∧ ∀ a ∈ l, f m ≤ f a → List.idxOf m l ≤ List.idxOf a l
-- Mathlib.Data.Finset.Lattice.Prod
Finset.inf'_sup_inf' : ∀ {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [inst : DistribLattice α] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty)
  (ht : t.Nonempty) (f : ι → α) (g : κ → α), s.inf' hs f ⊔ t.inf' ht g = (s ×ˢ t).inf' ⋯ fun i => f i.1 ⊔ g i.2
-- Mathlib.Analysis.Calculus.Deriv.Inv
deriv_div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'},
  DifferentiableAt 𝕜 c x →
    DifferentiableAt 𝕜 d x → d x ≠ 0 → deriv (c / d) x = (deriv c x * d x - c x * deriv d x) / d x ^ 2
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] (f : α → C) [inst_2 : CategoryTheory.Limits.HasCoproduct f],
  (CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone f).pt = ∐ f
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.has_cokernels : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.NonPreadditiveAbelian C],
  CategoryTheory.Limits.HasCokernels C
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.allRoots_nodup : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R], (RootPairing.EmbeddedG2.allRoots P).Nodup
-- Mathlib.Data.Set.Prod
Set.pi_nonempty_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)},
  (s.pi t).Nonempty ↔ ∀ (i : ι), ∃ x, i ∈ s → x ∈ t i
-- Init.Data.Option.Attach
Option.all_attachWith : ∀ {α : Type u_1} {p : α → Bool} {o : Option α} {r : α → Prop} (hr : ∀ (x : α), o = some x → r x)
  {q : { x // r x } → Bool}, (∀ (x : α) (h : r x), q ⟨x, h⟩ = p x) → Option.all q (o.attachWith r hr) = Option.all p o
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_eq_theta_add_sum_theta : ∀ {x : ℝ},
  2 ≤ x →
    Chebyshev.psi x = Chebyshev.theta x + ∑ n ∈ Finset.Icc 2 ⌊Real.log x / Real.log 2⌋₊, Chebyshev.theta (x ^ (1 / ↑n))
-- Mathlib.Data.Multiset.Powerset
/-- **Alias** of the reverse direction of `Multiset.nodup_powerset`. -/
Multiset.Nodup.powerset : ∀ {α : Type u_1} {s : Multiset α}, s.Nodup → s.powerset.Nodup
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertManyIfNewUnit_ind : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {ρ : Type w} [inst : ForIn Id ρ α] [inst_1 : EquivBEq α]
  [inst_2 : LawfulHashable α] {motive : (Std.ExtDHashMap α fun x => Unit) → Prop} (m : Std.ExtDHashMap α fun x => Unit)
  (l : ρ),
  motive m →
    (∀ (m : Std.ExtDHashMap α fun x => Unit) (a : α), motive m → motive (m.insertIfNew a ())) →
      motive (Std.ExtDHashMap.Const.insertManyIfNewUnit m l)
-- Mathlib.Probability.HasLaw
ProbabilityTheory.IndepFun.hasLaw_add : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {M : Type u_3} [inst : AddMonoid M]
  {mM : MeasurableSpace M} [MeasurableAdd₂ M] {μ ν : MeasureTheory.Measure M} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] {X Y : Ω → M},
  ProbabilityTheory.HasLaw X μ P →
    ProbabilityTheory.HasLaw Y ν P → ProbabilityTheory.IndepFun X Y P → ProbabilityTheory.HasLaw (X + Y) (μ.conv ν) P
-- Init.Data.Slice.List.Lemmas
ListSlice.toArray_mkSlice_rcc : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = (Std.Slice.toArray xs).extract lo (hi + 1)
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.instMulAction : {ι : Type u_1} →
  {α : Type u_3} → {A : ι → Type u_2} → [inst : Monoid α] → [(i : ι) → MulAction α (A i)] → MulAction α (GradedMonoid A)
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.coe_sSup' : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α} (S : Set ↥L), ↑(sSup S) = ⨆ N ∈ S, ↑N
-- Mathlib.NumberTheory.Dioph
/-- The constant function is Diophantine.  -/
Dioph.«termD._» : Lean.ParserDescr
-- Init.Data.Fin.Basic
Fin.neg_def : ∀ {n : ℕ} (a : Fin n), -a = ⟨(n - ↑a) % n, ⋯⟩
-- Init.Data.SInt.Basic
instOrOpInt32 : OrOp Int32
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_mapₘ : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → δ a},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.Raw.WFImp ↑(m.mapₘ f)
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.trace_mul_conjTranspose_self_eq_zero_iff : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : Fintype m] {R : Type u_5} [inst_2 : PartialOrder R]
  [inst_3 : NonUnitalRing R] [inst_4 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {A : Matrix m n R},
  (A * A.conjTranspose).trace = 0 ↔ A = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.ofEq_inv : ∀ {X : SSet} {x₀ x₁ y₀ y₁ : X.obj (Opposite.op { len := 0 })} {hom : SSet.Edge x₀ x₁} {hom' : SSet.Edge y₀ y₁}
  (I : hom.InvStruct) (hhom : hom.edge = hom'.edge), (I.ofEq hhom).inv = I.inv.ofEq ⋯ ⋯
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.fppfPrecoverage.eq_1 : AlgebraicGeometry.Scheme.fppfPrecoverage =
  AlgebraicGeometry.Scheme.precoverage (@AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.LocallyOfFinitePresentation)
-- Mathlib.Analysis.Matrix.Order
/-- The kronecker of two positive definite matrices is positive definite.  -/
Matrix.PosDef.kronecker : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [Finite n] {m : Type u_3} [Finite m] {x : Matrix n n 𝕜}
  {y : Matrix m m 𝕜}, x.PosDef → y.PosDef → (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) x y).PosDef
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- shift left by another BitVec expression. For constant shifts there exists a `BVUnop`.
 -/
Std.Tactic.BVDecide.BVExpr.shiftLeft : {m n : ℕ} → Std.Tactic.BVDecide.BVExpr m → Std.Tactic.BVDecide.BVExpr n → Std.Tactic.BVDecide.BVExpr m
-- Mathlib.Probability.Kernel.Disintegration.Unique
ProbabilityTheory.condKernel_compProd : ∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] (μ : MeasureTheory.Measure α) [inst_3 : MeasureTheory.IsFiniteMeasure μ]
  (κ : ProbabilityTheory.Kernel α Ω) [inst_4 : ProbabilityTheory.IsMarkovKernel κ], ⇑(μ.compProd κ).condKernel =ᵐ[μ] ⇑κ
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.instFunLikeCircle : {A : Type u_1} → [inst : Monoid A] → [inst_1 : TopologicalSpace A] → FunLike (PontryaginDual A) A Circle
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- The difference of two covariant derivatives, as a one-form taking values in the
endomorphisms of `V`.  -/
IsCovariantDerivativeOn.difference : {𝕜 : 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_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [inst_14 : FiberBundle F V] →
                                            {cov cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} →
                                              {s : Set M} →
                                                IsCovariantDerivativeOn F cov s →
                                                  IsCovariantDerivativeOn F cov' s →
                                                    [CompleteSpace 𝕜] →
                                                      [FiniteDimensional 𝕜 F] →
                                                        [inst_17 : VectorBundle 𝕜 F V] →
                                                          [ContMDiffVectorBundle 1 F V I] →
                                                            (x : M) → V x →L[𝕜] TangentSpace I x →L[𝕜] V x
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- If `P` is a submersive presentation of `S` as an `R`-algebra, `Ω[S⁄R]` is free.  -/
Algebra.SubmersivePresentation.free_kaehlerDifferential : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ), Module.Free S Ω[S⁄R]
-- Mathlib.Data.Multiset.ZeroCons
/-- Dependent recursor on multisets.
TODO: should be @[recursor 6], but then the definition of `Multiset.pi` fails with a stack
overflow in `whnf`.
 -/
Multiset.rec : {α : Type u_1} →
  {C : Multiset α → Sort u_3} →
    C 0 →
      (C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)) →
        (∀ (a a' : α) (m : Multiset α) (b : C m),
            C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)) →
          (m : Multiset α) → C m
-- Mathlib.Data.Finsupp.Single
Equiv.finsuppUnique_apply : ∀ {M : Type u_5} [inst : Zero M] {ι : Type u_13} [inst_1 : Unique ι] (a : ι →₀ M), Equiv.finsuppUnique a = a default
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.atEnd : {s : String.Slice} → String.Slice.Pattern.ForwardSliceSearcher s
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_rightUnitor_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b),
  Bicategory.Opposite.op2 (CategoryTheory.Bicategory.rightUnitor f).hom =
    (CategoryTheory.Bicategory.leftUnitor f.op).hom
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.ae_tendsto_enorm : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] {F' : ℕ → α → ε} {f' : α → ε},
  (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F' n a) Filter.atTop (nhds (f' a))) →
    ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => ‖F' n a‖ₑ) Filter.atTop (nhds ‖f' a‖ₑ)
-- Init.Data.List.Find
List.IsSuffix.lookup_eq_none : ∀ {α : Type u_2} [inst : BEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)},
  l₁ <:+ l₂ → List.lookup k l₂ = none → List.lookup k l₁ = none
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.handleDocumentSymbol : Lean.Lsp.DocumentSymbolParams → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.DocumentSymbolResult)
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.mk_toPSet : ∀ (o : Ordinal.{u_1}), ZFSet.mk o.toPSet = o.toZFSet
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.mapDomain_id : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {v : SkewMonoidAlgebra k G},
  (SkewMonoidAlgebra.mapDomain id) v = v
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flipEquivalence_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Square.flipEquivalence.unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Square C))