mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulPosMono.to_covariantClass_pos_mul_le : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulPosMono α],
  CovariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x1 x2 => x1 ≤ x2
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.instNonemptyState : Nonempty Std.Http.Body.Channel.State✝
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
/-- Fold a bilinear map along the generators of a term of the clifford algebra, with the rule
given by `foldr' Q f hf n (ι Q m * x) = f m (x, foldr' Q f hf n x)`.
Note this is like `CliffordAlgebra.foldr`, but with an extra `x` argument.
Implement the recursion scheme `F[n0](m * x) = f(m, (x, F[n0](x)))`.  -/
CliffordAlgebra.foldr' : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                (Q : QuadraticForm R M) →
                  (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N) →
                    (∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
                        (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx) →
                      N → CliffordAlgebra Q →ₗ[R] N
-- Batteries.Recycling.MonadSatisfying.Basic
/-- `SatisfiesM` distributes over `>>=`, weakest precondition version.  -/
SatisfiesM.bind_pre : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} {q : β → Prop} {x : m α} [inst : Monad m] [LawfulMonad m] {f : α → m β},
  SatisfiesM (fun a => SatisfiesM q (f a)) x → SatisfiesM q (x >>= f)
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- `F` is equivalent to `F` as an intermediate field of `E / K`.
 -/
IntermediateField.restrictAlgEquiv : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → {F E : IntermediateField K L} → (h : F ≤ E) → ↥F ≃ₐ[K] ↥(IntermediateField.restrict h)
-- Mathlib.NumberTheory.MulChar.Lemmas
MulChar.ofRootOfUnity_spec : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : Fintype M] [inst_2 : DecidableEq M] {R : Type u_2}
  [inst_3 : CommMonoidWithZero R] {ζ : Rˣ} (hζ : ζ ∈ rootsOfUnity (Fintype.card Mˣ) R) {g : Mˣ}
  (hg : ∀ (x : Mˣ), x ∈ Subgroup.zpowers g), (MulChar.ofRootOfUnity hζ hg) ↑g = ↑ζ
-- Mathlib.Data.Finset.Sum
Finset.inl_mem_disjSum : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {a : α}, Sum.inl a ∈ s.disjSum t ↔ a ∈ s
-- Init.Data.List.TakeDrop
List.drop_eq_getElem_cons : ∀ {α : Type u_1} {i : ℕ} {l : List α} (h : i < l.length), List.drop i l = l[i] :: List.drop (i + 1) l
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
MeasureTheory.eLpNorm'_add_le_of_le_one : ∀ {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε]
  {q : ℝ} {μ : MeasureTheory.Measure α} {f g : α → ε},
  MeasureTheory.AEStronglyMeasurable f μ →
    0 ≤ q →
      q ≤ 1 →
        MeasureTheory.eLpNorm' (f + g) q μ ≤
          2 ^ (1 / q - 1) * (MeasureTheory.eLpNorm' f q μ + MeasureTheory.eLpNorm' g q μ)
-- Mathlib.LinearAlgebra.Basis.Exact
Module.Basis.ofSplitExact_apply : ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K] [inst_6 : Module R P]
  {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K} (hs : s ∘ₗ f = LinearMap.id) (hfg : Function.Exact ⇑f ⇑g)
  {ι : Type u_5} {κ : Type u_6} {σ : Type u_7} {a : κ → ι} {b : σ → ι} (hg : Function.Surjective ⇑g)
  (v : Module.Basis ι R M) (hainj : Function.Injective a) (hsa : ∀ (i : κ), s (v (a i)) = 0)
  (hlib : LinearIndependent R (⇑s ∘ ⇑v ∘ b)) (hab : Codisjoint (Set.range a) (Set.range b)) (k : κ),
  (Module.Basis.ofSplitExact hs hfg hg v hainj hsa hlib hab) k = g (v (a k))
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.instFaithfulObjPost : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor T D) [F.Faithful], (CategoryTheory.Under.post F).Faithful
-- Mathlib.Analysis.Normed.Operator.Extend
LinearEquiv.extend_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6}
  [inst : NormedDivisionRing 𝕜] [inst_1 : NormedDivisionRing 𝕜₂] [inst_2 : AddCommGroup E]
  [inst_3 : NormedAddCommGroup Eₗ] [inst_4 : AddCommGroup F] [inst_5 : NormedAddCommGroup Fₗ] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 Eₗ] [inst_8 : IsBoundedSMul 𝕜 Eₗ] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₂ Fₗ]
  [inst_11 : IsBoundedSMul 𝕜₂ Fₗ] [inst_12 : CompleteSpace Eₗ] [inst_13 : CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_14 : RingHomInvPair σ₁₂ σ₂₁] [inst_15 : RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F)
  (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖)
  (h_dense₂ : DenseRange ⇑e₂) (h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖) (x : Eₗ),
  (f.extend e₁ e₂ h_dense₁ h_norm₁ h_dense₂ h_norm₂) x = ((e₂ ∘ₛₗ ↑f).extendOfNorm e₁) x
-- Mathlib.Order.Atoms
IsStronglyAtomic.isAtomic : ∀ (α : Type u_5) [inst : PartialOrder α] [inst_1 : OrderBot α] [IsStronglyAtomic α], IsAtomic α
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueSums.toTwoUniqueSums_of_addGroup : ∀ {G : Type u_1} [inst : AddGroup G] [UniqueSums G], TwoUniqueSums G
-- Mathlib.Data.Set.Lattice.Image
Set.mapsTo_sInter : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {T : Set (Set β)} {f : α → β},
  Set.MapsTo f s (⋂₀ T) ↔ ∀ t ∈ T, Set.MapsTo f s t
-- Mathlib.LinearAlgebra.Dimension.LinearMap
LinearMap.rank_comp_le_left : ∀ {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [inst : Semiring K] [inst_1 : AddCommMonoid V]
  [inst_2 : Module K V] [inst_3 : AddCommMonoid V'] [inst_4 : Module K V'] [inst_5 : AddCommMonoid V'']
  [inst_6 : Module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V''), (f ∘ₗ g).rank ≤ f.rank
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.liesOver_map_of_isPrime_disjoint : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {I : Ideal R} [I.IsPrime],
  Disjoint ↑M ↑I → (Ideal.map (algebraMap R S) I).LiesOver I
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.revSkip?_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String} {pos : s.Pos},
  pos.toSlice.revSkip? pat = Option.map String.Pos.toSlice (pos.revSkip? pat)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addIndex_empty : ∀ {G : Type u_1} [inst : AddGroup G] {V : Set G}, MeasureTheory.Measure.haar.addIndex ∅ V = 0
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agmSequences_fst_monotone : ∀ {x y : NNReal}, Monotone fun n => (x.agmSequences y n).1
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.compLeft_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (ψ : S₃ ⟶ S₁), (h.compLeft ψ).h₀ = CategoryTheory.CategoryStruct.comp ψ.τ₁ h.h₀
-- Mathlib.Algebra.Order.Sub.Basic
tsub_pos_of_lt : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, a < b → 0 < b - a
-- Mathlib.RingTheory.Algebraic.MvPolynomial
MvPolynomial.transcendental_polynomial_aeval_X : ∀ {σ : Type u_1} (R : Type u_2) [inst : CommRing R] (i : σ) {f : Polynomial R},
  Transcendental R f → Transcendental R ((Polynomial.aeval (MvPolynomial.X i)) f)
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.prod_iso_toFun : ∀ (R : Type u_1) [inst : CommRing R] (K : Type u_2) [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] (L : Type u_3)
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (a : K ⋊⁅0⁆ L),
  (LieAlgebra.SemiDirectSum.prod_iso R K L) a = (a.left, a.right)
-- Mathlib.Data.List.Map2
List.zipRight_nil_left : ∀ {α : Type u} {β : Type v} (bs : List β), [].zipRight bs = List.map (fun b => (none, b)) bs
-- Lean.Level
_private.Lean.Level.0.Lean.Level.geq.go.match_1.eq_4 : ∀ (motive : Lean.Level → Lean.Level → Sort u_1) (a u₂ v : Lean.Level)
  (h_1 : (x : Lean.Level) → motive x Lean.Level.zero) (h_2 : (u v₁ v₂ : Lean.Level) → motive u (v₁.max v₂))
  (h_3 : (u₁ u₂ v : Lean.Level) → motive (u₁.max u₂) v) (h_4 : (a u₂ v : Lean.Level) → motive (a.imax u₂) v)
  (h_5 : (u v : Lean.Level) → motive u.succ v.succ) (h_6 : (x x_1 : Lean.Level) → motive x x_1),
  (v = Lean.Level.zero → False) →
    (∀ (v₁ v₂ : Lean.Level), v = v₁.max v₂ → False) →
      (match a.imax u₂, v with
        | x, Lean.Level.zero => h_1 x
        | u, v₁.max v₂ => h_2 u v₁ v₂
        | u₁.max u₂, v => h_3 u₁ u₂ v
        | a.imax u₂, v => h_4 a u₂ v
        | u.succ, v.succ => h_5 u v
        | x, x_1 => h_6 x x_1) =
        h_4 a u₂ v
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- (Implementation). The morphism `ℱ(X) ⟶ ℱ'(X)` given by gluing the `pushforwardFamily`.  -/
CategoryTheory.Functor.IsCoverDense.Types.appHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {K : CategoryTheory.GrothendieckTopology D} →
          {G : CategoryTheory.Functor C D} →
            {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} →
              {ℱ' : CategoryTheory.Sheaf K (Type v)} →
                (G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) →
                  [G.IsCoverDense K] →
                    [G.IsLocallyFull K] → (X : D) → ℱ.obj (Opposite.op X) ⟶ ℱ'.obj.obj (Opposite.op X)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.instDecidableMemOfTransCmp : {α : Type u_1} → {cmp : α → α → Ordering} → {x : α} → [Std.TransCmp cmp] → {t : RBTree.RBSet α cmp} → Decidable (x ∈ t)
-- Batteries.Data.Array.Merge
Array.mergeDedupWith.go.eq_def : ∀ {α : Type u_1} [ord : Ord α] (xs ys : Array α) (merge : α → α → α) (acc : Array α) (i j : ℕ),
  Array.mergeDedupWith.go xs ys merge acc i j =
    if hi : i ≥ xs.size then
      acc ++
        ↑(have a := ys;
          a.toSubarray j)
    else
      if hj : j ≥ ys.size then
        acc ++
          ↑(have a := xs;
            a.toSubarray i)
      else
        have x := xs[i];
        have y := ys[j];
        match compare x y with
        | Ordering.lt => Array.mergeDedupWith.go xs ys merge (acc.push x) (i + 1) j
        | Ordering.gt => Array.mergeDedupWith.go xs ys merge (acc.push y) i (j + 1)
        | Ordering.eq => Array.mergeDedupWith.go xs ys merge (acc.push (merge x y)) (i + 1) (j + 1)
-- Mathlib.CategoryTheory.EpiMono
/-- A constructor for `IsSplitEpi f` taking a `SplitEpi f` as an argument  -/
CategoryTheory.IsSplitEpi.mk' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (se : CategoryTheory.SplitEpi f),
  CategoryTheory.IsSplitEpi f
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.AB5OfSize_shrink : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasFilteredColimitsOfSize.{max w w₂, max w' w₂', v, u} C]
  [CategoryTheory.AB5OfSize.{max w w₂, max w' w₂', v, u} C], CategoryTheory.AB5OfSize.{w, w', v, u} C
-- Mathlib.Algebra.Notation.Defs
sub_dite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Sub α] (a : α) (b : P → α) (c : ¬P → α),
  (a - if h : P then b h else c h) = if h : P then a - b h else a - c h
-- Lean.Meta.Sym.Pattern
/-- Like `mkPatternFromDeclWithKey`, but for a complex proof expression instead of the declaration of a
theorem.
 -/
Lean.Meta.Sym.mkPatternFromExprWithKey : {α : Type} →
  Lean.Expr →
    optParam (List Lean.Name) [] →
      (Lean.Expr → Lean.MetaM (Lean.Expr × α)) → optParam Bool false → Lean.MetaM (Lean.Meta.Sym.Pattern × α)
-- Mathlib.NumberTheory.LSeries.Basic
/-- The L-series of `δ` is the constant function `1`.  -/
LSeries_delta : LSeries LSeries.delta = 1
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.i₀_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (self : HomotopicalAlgebra.Precylinder A) {Z : C}
  (h : A ⟶ Z), CategoryTheory.CategoryStruct.comp self.i₀ (CategoryTheory.CategoryStruct.comp self.π h) = h
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesLimits.liftedCone_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra)
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Monad.ForgetCreatesLimits.liftedCone D c t).pt =
    CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t
-- Mathlib.Probability.Distributions.Uniform
/-- The density of the uniform measure on a set with respect to itself. This allows us to abstract
away the choice of random variable and probability space.  -/
MeasureTheory.pdf.uniformPDF : {E : Type u_1} →
  [inst : MeasurableSpace E] →
    Set E → E → autoParam (MeasureTheory.Measure E) MeasureTheory.pdf.uniformPDF._auto_1 → ENNReal
-- Std.Data.ExtTreeSet.Basic
/-- Returns `true` if `a`, or an element equal to `a` according to the comparator `cmp`, is contained
in the set. There is also a `Prop`-valued version of this: `a ∈ t` is equivalent to
`t.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
`==` for equality checks, while for tree sets, both use the given comparator `cmp`.
 -/
Std.ExtTreeSet.contains : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → Bool
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opCounitIso.eq_1 : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V],
  HomologicalComplex.opCounitIso V c =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        HomologicalComplex.Hom.isoOfComponents
          (fun x =>
            CategoryTheory.Iso.refl
              ((((HomologicalComplex.opInverse V c).comp (HomologicalComplex.opFunctor V c)).obj X).X x))
          ⋯)
      ⋯
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.entryAtIdx? : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → ℕ → Option ((a : α) × β a)
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instIsCharPInt8HPowNatOfNat : Lean.Grind.IsCharP Int8 (2 ^ 8)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.equiv_iff_keys_unit_perm : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Std.HashMap.Raw α Unit},
  m₁.Equiv m₂ ↔ m₁.keys.Perm m₂.keys
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The Law of Quadratic Reciprocity for the Jacobi symbol: if `a` and `b` are natural numbers
with `a % 4 = 1` and `b` odd, then `J(a | b) = J(b | a)`.  -/
jacobiSym.quadratic_reciprocity_one_mod_four : ∀ {a b : ℕ}, a % 4 = 1 → Odd b → jacobiSym (↑a) b = jacobiSym (↑b) a
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localRingHom.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime]
  (J : Ideal P) [inst_2 : J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J),
  Localization.localRingHom I J f hIJ = IsLocalization.map (Localization.AtPrime J) f ⋯
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.fixingSubgroup_of_insert : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] (a : α)
  (s : Set ↥(SubMulAction.ofStabilizer M a)),
  fixingSubgroup M (insert a ((fun x => ↑x) '' s)) =
    Subgroup.map (MulAction.stabilizer M a).subtype (fixingSubgroup (↥(MulAction.stabilizer M a)) s)
-- Init.Data.Order.PackageFactories
Std.FactoryInstances.beqOfDecidableLE : {α : Type u} → [inst : LE α] → [DecidableLE α] → BEq α
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedMinOfIsClosedUnderIsomorphisms_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P P' : CategoryTheory.ObjectProperty C) [P.IsTriangulated] [P.IsClosedUnderIsomorphisms] [P'.IsTriangulated],
  (P ⊓ P').IsTriangulated
-- Mathlib.Tactic.Linarith.Frontend
/-- Discharger to prove that a candidate linear combination of hypothesis is zero.
In a tactic configuration, set using `(discharger := by ...)` notation.  -/
Mathlib.Tactic.Linarith.LinarithConfig.discharger : Mathlib.Tactic.Linarith.LinarithConfig → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
IsCovariantDerivativeOn.smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [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 : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {s : Set M},
  IsCovariantDerivativeOn F cov s →
    ∀ {σ : (x : M) → V x} {x : M} (a : 𝕜),
      MDiffAt (T% σ) x → autoParam (x ∈ s) IsCovariantDerivativeOn.smul_const._auto_1 → cov (a • σ) x = a • cov σ x
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.isRegular : Lean.Elab.Term.Do.ToTerm.Kind → Bool
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval.eq_1 : ∀ {w : ℕ} (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (idx : ℕ),
  Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.var idx) =
    if h : (assign.get idx).w = w then h ▸ (assign.get idx).bv else BitVec.truncate w (assign.get idx).bv
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstPowNat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_lift : ∀ {X : AlgebraicGeometry.Scheme},
  QuasiSeparatedSpace ↥X ↔
    AlgebraicGeometry.QuasiCompact
      (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
-- Mathlib.Algebra.Order.Star.Basic
IsUnit.star_left_conjugate_nonneg_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R] {u x : R},
  IsUnit u → (0 ≤ star u * x * u ↔ 0 ≤ x)
-- Mathlib.Algebra.Algebra.Pi
AlgEquiv.piCongrRight_apply : ∀ {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} {A₂ : ι → Type u_6} [inst : CommSemiring R]
  [inst_1 : (i : ι) → Semiring (A₁ i)] [inst_2 : (i : ι) → Semiring (A₂ i)] [inst_3 : (i : ι) → Algebra R (A₁ i)]
  [inst_4 : (i : ι) → Algebra R (A₂ i)] (e : (i : ι) → A₁ i ≃ₐ[R] A₂ i) (x : (i : ι) → A₁ i) (j : ι),
  (AlgEquiv.piCongrRight e) x j = (e j) (x j)
-- Mathlib.Topology.Constructions.SumProd
instTopologicalSpaceSum : {X : Type u} → {Y : Type v} → [t₁ : TopologicalSpace X] → [t₂ : TopologicalSpace Y] → TopologicalSpace (X ⊕ Y)
-- Batteries.Data.BinomialHeap.Lemmas
Batteries.BinomialHeap.Imp.Heap.size.eq_1 : ∀ {α : Type u_1}, Batteries.BinomialHeap.Imp.Heap.nil.size = 0
-- Mathlib.Order.Defs.LinearOrder
max_def : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), max a b = if a ≤ b then b else a
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst_assoc : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m')
  (hm' : 0 < m') {x : A} (hx : x = f * g) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)
          (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm'))
        h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) h
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.neg_Z : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R), W'.neg P 2 = P 2
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.erase_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a : α},
  ∅.erase a = ∅
-- Init.Data.UInt.Lemmas
UInt16.div_zero : ∀ {a : UInt16}, a / 0 = 0
-- Batteries.Tactic.PrintPrefix
Batteries.Tactic.PrintPrefixConfig.mk.inj : ∀
  {imported propositions propositionsOnly showTypes internals imported_1 propositions_1 propositionsOnly_1 showTypes_1
    internals_1 : Bool},
  { imported := imported, propositions := propositions, propositionsOnly := propositionsOnly, showTypes := showTypes,
        internals := internals } =
      { imported := imported_1, propositions := propositions_1, propositionsOnly := propositionsOnly_1,
        showTypes := showTypes_1, internals := internals_1 } →
    imported = imported_1 ∧
      propositions = propositions_1 ∧
        propositionsOnly = propositionsOnly_1 ∧ showTypes = showTypes_1 ∧ internals = internals_1
-- Mathlib.Data.Part
Part.some_toOption : ∀ {α : Type u_1} (a : α) [inst : Decidable (Part.some a).Dom], (Part.some a).toOption = some a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.map_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z} {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) F]
  [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span f g) F],
  CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g i →
    (CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i) ↔ CategoryTheory.IsPushout f g h i)
-- Mathlib.Algebra.Lie.Basis.Base
LieAlgebra.Basis.linearIndepOn_root_baseSupp : ∀ {ι : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Fintype ι] [inst_1 : Field K] [inst_2 : CharZero K]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  (b : LieAlgebra.Basis ι H) [inst_6 : LieModule.IsTriangularizable K (↥H) L] [inst_7 : LieAlgebra.IsKilling K L],
  LinearIndepOn K (⇑(LieAlgebra.IsKilling.rootSystem H).root) (Set.range b.baseSupp')
-- Mathlib.GroupTheory.GroupAction.Jordan
/-- A primitive subgroup of `Equiv.Perm α` that contains a swap
is the full permutation group (Jordan).  -/
Equiv.Perm.subgroup_eq_top_of_isPreprimitive_of_isSwap_mem : ∀ {α : Type u_1} {G : Subgroup (Equiv.Perm α)} [inst : DecidableEq α] [Finite α],
  MulAction.IsPreprimitive (↥G) α → ∀ (g : Equiv.Perm α), g.IsSwap → g ∈ G → G = ⊤
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Matrix.mem_spectrum_iff_not_isUnit_eval_charpoly : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R] {B : Matrix n n R}
  {r : R}, r ∈ spectrum R B ↔ ¬IsUnit (Polynomial.eval r B.charpoly)
-- Lean.Util.Path
/-- Infer module name of source file name.  -/
Lean.moduleNameOfFileName : System.FilePath → Option System.FilePath → IO Lean.Name