mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Ultrafilter.Basic
Filter.compl_mem_hyperfilter_of_finite : ∀ {α : Type u} [inst : Infinite α] {s : Set α}, s.Finite → sᶜ ∈ Filter.hyperfilter α
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.addZeroClass.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Zero M₁] [inst_2 : AddZeroClass M₂] (f : M₁ → M₂)
  (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y),
  Function.Injective.addZeroClass f hf one mul = { toZero := inst_1, toAdd := inst, zero_add := ⋯, add_zero := ⋯ }
-- Mathlib.Data.Nat.Sqrt
Nat.log2_two : Nat.log2 2 = 1
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddGroupOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : AddGroup Mᵃᵒᵖ], DomAddAct.instAddGroupOfAddOpposite = inst
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.real_smul_negPart_nonneg : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : ℝ),
  0 ≤ r → (r • j).negPart = r.toNNReal • j.negPart
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dec.sizeOf_spec : ∀ (h : Lean.FVarId), sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dec h) = 1 + sizeOf h
-- Mathlib.RingTheory.Polynomial.GaussNorm
/-- Given a polynomial `p` in `R[X]`, a function `v : R → ℝ` and a real number `c`, the Gauss norm
is defined as the supremum of the set of all values of `v (p.coeff i) * c ^ i` for all `i` in the
support of `p`.  -/
Polynomial.gaussNorm : {R : Type u_1} → {F : Type u_2} → [inst : Semiring R] → [FunLike F R ℝ] → F → ℝ → Polynomial R → ℝ
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonRpcOptions : Lean.ToJson Lean.Lsp.RpcOptions
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.slash_def : ∀ {k : ℤ} (f : UpperHalfPlane → ℂ) (g : GL (Fin 2) ℝ),
  SlashAction.map k g f = fun τ =>
    (UpperHalfPlane.σ g) (f (g • τ)) * ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k - 1) *
      UpperHalfPlane.denom g ↑τ ^ (-k)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_of_contains_insertMany!_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l) = true →
        (List.map Prod.fst l).contains k = false → Std.DTreeMap.Internal.Impl.contains k t = true
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- Morphism of additive `C^n` monoids.  -/
ContMDiffAddMonoidMorphism : {𝕜 : 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] →
              {H' : Type u_5} →
                [inst_4 : TopologicalSpace H'] →
                  {E' : Type u_6} →
                    [inst_5 : NormedAddCommGroup E'] →
                      [inst_6 : NormedSpace 𝕜 E'] →
                        ModelWithCorners 𝕜 E H →
                          ModelWithCorners 𝕜 E' H' →
                            WithTop ℕ∞ →
                              (G : Type u_8) →
                                [inst : TopologicalSpace G] →
                                  [ChartedSpace H G] →
                                    [AddMonoid G] →
                                      (G' : Type u_9) →
                                        [inst : TopologicalSpace G'] →
                                          [ChartedSpace H' G'] → [AddMonoid G'] → Type (max u_8 u_9)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverse_dropLast : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.dropLast.reverse = p.reverse.tail.copy ⋯ ⋯
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.homQuotientZPowOfHom.eq_1 : ∀ {A B : Type u} [inst : CommGroup A] [inst_1 : CommGroup B] (f : A →* B) (n : ℤ),
  QuotientGroup.homQuotientZPowOfHom f n =
    QuotientGroup.lift (zpowGroupHom n).range ((QuotientGroup.mk' (zpowGroupHom n).range).comp f) ⋯
-- Lean.Meta.Match.MVarRenaming
Lean.Meta.MVarRenaming.mk.inj : ∀ {map map_1 : Lean.MVarIdMap Lean.MVarId}, { map := map } = { map := map_1 } → map = map_1
-- Mathlib.NumberTheory.NumberField.Ideal.Basic
Ideal.rootsOfUnityMapQuot_injective : ∀ {K : Type u_1} [inst : Field K] {I : Ideal (NumberField.RingOfIntegers K)} [inst_1 : NumberField K] (n : ℕ)
  [NeZero n], Ideal.absNorm I ≠ 1 → (Ideal.absNorm I).Coprime n → Function.Injective ⇑(I.rootsOfUnityMapQuot n)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₄_of_isCharTwoJEqZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF], W.c₄ = -48 * W.a₄
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.iff_bijective : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes},
  c.IsColimit →
    ∀ {c' : F.CoconeTypes} (f : c.pt → c'.pt),
      (∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)) → (c'.IsColimit ↔ Function.Bijective f)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.Rewrites.input_output : ∀ {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N}, r.Rewrites [Symbol.nonterminal r.input] r.output
-- Mathlib.Topology.Bases
TopologicalSpace.instFirstCountableTopologyForallOfCountable : ∀ {ι : Type u_1} {X : ι → Type u_2} [Countable ι] [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), FirstCountableTopology (X i)], FirstCountableTopology ((i : ι) → X i)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_le : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : Preorder ι] {s : ι → Set Ω},
  (∀ (n : ι), MeasurableSet (s n)) →
    ProbabilityTheory.iCondIndepSet m' hm' s μ →
      ∀ (i : ι) {k : ι},
        i < k →
          ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {s k})
            (MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t}) hm' μ
-- Mathlib.LinearAlgebra.BilinearForm.DualLattice
LinearMap.BilinForm.dualSubmodule_span_of_basis : ∀ {R : Type u_4} {S : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : Field S] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (B : LinearMap.BilinForm S M) {ι : Type u_1} [inst_7 : Finite ι] [inst_8 : DecidableEq ι] (hB : B.Nondegenerate)
  (b : Module.Basis ι S M),
  B.dualSubmodule (Submodule.span R (Set.range ⇑b)) = Submodule.span R (Set.range ⇑(B.dualBasis hB b))
-- Lean.Elab.Do.Control
/-- Substack at which the `continue` handler was installed, if any.  -/
Lean.Elab.Do.EffectForwarder.continueBase? : Lean.Elab.Do.EffectForwarder → Option Lean.Elab.Do.ControlStack
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atBot_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α), ∀ᵐ (t : β) ∂ν a, Filter.Tendsto (f (a, t)) Filter.atBot (nhds 0)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_neg_one : ∀ (x : NNReal), x ^ (-1) = x⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- A kernel fork is just a fork where the second morphism is a zero morphism.  -/
CategoryTheory.Limits.KernelFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] → {X Y : C} → (X ⟶ Y) → Type (max u v)
-- Mathlib.CategoryTheory.Core
CategoryTheory.Iso.coreId : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}, (CategoryTheory.Iso.refl F).core = CategoryTheory.Iso.refl F.core
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_iInf : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {ι : Sort u_5} (f : M →ₙ* N) (s : ι → Subsemigroup N),
  Subsemigroup.comap f (iInf s) = ⨅ i, Subsemigroup.comap f (s i)
-- Mathlib.AlgebraicGeometry.SpreadingOut
AlgebraicGeometry.instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X) [X.IsGermInjectiveAt x] [AlgebraicGeometry.IsOpenImmersion f],
  Y.IsGermInjectiveAt (f x)
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
/-- The natural embedding of the free semigroup into the free monoid.
This is injective (`FreeSemigroup.toFreeMonoid_injective`), and its image
consists of all non-`1` elements of the free monoid (`FreeSemigroup.eq_one_or_toFreeMonoid`).
 -/
FreeSemigroup.toFreeMonoid : {α : Type u_1} → FreeSemigroup α →ₙ* FreeMonoid α
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A]
  (X Y : CategoryTheory.Sheaf J A),
  (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y).hom =
    CategoryTheory.SemiCartesianMonoidalCategory.snd X.obj Y.obj
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
QuadraticMap.add_toBilin : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : LinearOrder ι] [inst_1 : CommRing R]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  (bm : Module.Basis ι R M) (Q₁ Q₂ : QuadraticMap R M N), (Q₁ + Q₂).toBilin bm = Q₁.toBilin bm + Q₂.toBilin bm
-- Lean.Attributes
Lean.ParametricAttribute.setParam : {α : Type} → Lean.ParametricAttribute α → Lean.Environment → Lean.Name → α → Except String Lean.Environment
-- Std.Internal.Do.Order.Basic
/-- `x ⊑ ⌜p⌝` whenever `p` holds.  -/
Lean.Order.le_ofProp : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l] (x : l) (p : Prop),
  p → Lean.Order.PartialOrder.rel x (Lean.Order.CompleteLattice.ofProp p)
-- Mathlib.CategoryTheory.Limits.Comma
/-- Let `F : J ⥤ Comma L R`. If `R` preserves the limit of
`F ⋙ snd _ _`, then `Comma.fst L R` and `Comma.snd L R` jointly
reflect the limit of `F`, i.e. if `c` is a cone for `F` which
becomes a limit after applying `Comma.fst L R` and `Comma.snd L R`,
then `c` is a limit.  -/
CategoryTheory.Comma.fstSndJointlyReflectLimit : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {A : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        {B : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} B] →
            {T : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} T] →
                {L : CategoryTheory.Functor A T} →
                  {R : CategoryTheory.Functor B T} →
                    {F : CategoryTheory.Functor J (CategoryTheory.Comma L R)} →
                      {c : CategoryTheory.Limits.Cone F} →
                        [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] →
                          CategoryTheory.Limits.IsLimit ((CategoryTheory.Comma.fst L R).mapCone c) →
                            CategoryTheory.Limits.IsLimit ((CategoryTheory.Comma.snd L R).mapCone c) →
                              CategoryTheory.Limits.IsLimit c
-- Lean.Elab.Do.Basic
/-- Given a continuation `dec` and a reference `ref`, returns a continuation derived from `dec` with result type `PUnit`.
If `dec` already has result type `PUnit`, simply returns `dec`. Otherwise, an error is logged and a
new continuation is returned that calls `dec` with `sorry` as a result. The error is reported at `ref`.
 -/
Lean.Elab.Do.DoElemCont.ensureUnitAt : Lean.Elab.Do.DoElemCont → Lean.Syntax → Lean.Elab.Do.DoElabM Lean.Elab.Do.DoElemCont
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- If two lifts of circle homeomorphisms have the same translation number, then they are
semiconjugate by a `CircleDeg1Lift`. This version uses assumptions `bijective f₁` and
`bijective f₂` to assume that `f₁` and `f₂` are homeomorphisms.  -/
CircleDeg1Lift.semiconj_of_bijective_of_translationNumber_eq : ∀ {f₁ f₂ : CircleDeg1Lift},
  Function.Bijective ⇑f₁ →
    Function.Bijective ⇑f₂ → f₁.translationNumber = f₂.translationNumber → ∃ F, Function.Semiconj ⇑F ⇑f₁ ⇑f₂
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contSupp.eq_1 : ∀ (fs : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.contSupp (Turing.PartrecToTM2.Cont'.cons₁ fs k) =
    Turing.PartrecToTM2.trStmts₁
        (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.main Turing.PartrecToTM2.K'.aux
          (Turing.PartrecToTM2.move₂ (fun s => decide (s = Turing.PartrecToTM2.Γ'.consₗ)) Turing.PartrecToTM2.K'.stack
            Turing.PartrecToTM2.K'.main
            (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.aux Turing.PartrecToTM2.K'.stack
              (Turing.PartrecToTM2.trNormal fs k.cons₂)))) ∪
      (Turing.PartrecToTM2.codeSupp' fs k.cons₂ ∪
        (Turing.PartrecToTM2.trStmts₁
            (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret k)) ∪
          Turing.PartrecToTM2.contSupp k))
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
IsCovariantDerivativeOn.add : ∀ {𝕜 : 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 : optParam (Set M) Set.univ},
  IsCovariantDerivativeOn F cov s →
    ∀ {σ σ' : (x : M) → V x} {x : M},
      MDiffAt (T% σ) x →
        MDiffAt (T% σ') x → autoParam (x ∈ s) IsCovariantDerivativeOn._auto_1 → cov (σ + σ') x = cov σ x + cov σ' x
-- Lean.Compiler.IR.Basic
Lean.IR.instAlphaEqvArrayArg : Lean.IR.AlphaEqv (Array Lean.IR.Arg)
-- Mathlib.Topology.MetricSpace.Holder
/-- If a function is Hölder over a bounded set, then it is bounded.  -/
HolderOnWith.holderOnWith_zero_of_bounded : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {C D : NNReal} {A : Set X},
  (∀ x ∈ A, ∀ y ∈ A, edist x y ≤ ↑D) → HolderOnWith C r f A → HolderOnWith (C * D ^ ↑r) 0 f A
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.equivFunctor_apply : ∀ (C D : CategoryTheory.Cat) (a : CategoryTheory.Cat.of ↑C ⟶ CategoryTheory.Cat.of ↑D),
  (CategoryTheory.Cat.Hom.equivFunctor C D) a = a.toFunctor
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coeFn_smul : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E] (c : 𝕜)
  (f : ↥(MeasureTheory.Lp E p μ)), ↑↑(c • f) =ᵐ[μ] c • ↑↑f
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.Functor.PreservesHomology.mk : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D}
  [inst_4 : F.PreservesZeroMorphisms],
  autoParam (∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F)
      CategoryTheory.Functor.PreservesHomology.preservesKernels._autoParam →
    autoParam
        (∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F)
        CategoryTheory.Functor.PreservesHomology.preservesCokernels._autoParam →
      F.PreservesHomology
-- Mathlib.Order.Types.Defs
/-- The order is defined so that `type α ≤ type β` iff there exists an order embedding `α ↪o β`.
 -/
OrderType.instPreorder : Preorder OrderType.{u_1}
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
/-- The projection is `0` if and only if all the elements have norm `0`.  -/
SeparationQuotient.normedMk_eq_zero_iff : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M], SeparationQuotient.normedMk = 0 ↔ ∀ (x : M), ‖x‖ = 0
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.Cotangent.lift_surjective_iff : ∀ {R : Type u} [inst : CommRing R] {S : Type u_3} [inst_1 : CommRing S] [inst_2 : Algebra R S] {I : Ideal S}
  {M : Type u_4} [inst_3 : AddCommGroup M] [inst_4 : Module R M] (f : ↥I →ₗ[R] M) (hf : ∀ (x y : ↥I), f (x * y) = 0),
  Function.Surjective ⇑(Ideal.Cotangent.lift f hf) ↔ Function.Surjective ⇑f
-- Mathlib.Algebra.Lie.Basic
LieRing.toAddCommGroup : {L : Type v} → [self : LieRing L] → AddCommGroup L
-- Init.Internal.Order.Lemmas
Lean.Order.List.monotone_foldrM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → α → β → m β) (init : β) (xs : List α),
  Lean.Order.monotone f → Lean.Order.monotone fun x => List.foldrM (f x) init xs
-- Mathlib.SetTheory.Ordinal.Notation
NONote.instToString : ToString NONote
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trPosNum.match_1.eq_1 : ∀ (motive : PosNum → Sort u_1) (h_1 : Unit → motive PosNum.one) (h_2 : (n : PosNum) → motive n.bit0)
  (h_3 : (n : PosNum) → motive n.bit1),
  (match PosNum.one with
    | PosNum.one => h_1 ()
    | n.bit0 => h_2 n
    | n.bit1 => h_3 n) =
    h_1 ()
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.trW_iff_of_distinguished' : ∀ {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 : CategoryTheory.ObjectProperty C) [P.IsStableUnderShift ℤ] [P.IsClosedUnderIsomorphisms],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P.trW T.mor₂ ↔ P T.obj₁
-- Mathlib.Tactic.Linarith.Frontend
/-- `linarith` attempts to find a contradiction between hypotheses that are linear (in)equalities.
Equivalently, it can prove a linear inequality by assuming its negation and proving `False`.

In theory, `linarith` should prove any goal that is true in the theory of linear arithmetic over
the rationals. While there is some special handling for non-dense orders like `Nat` and `Int`,
this tactic is not complete for these theories and will not prove every true goal. It will solve
goals over arbitrary types that instantiate `CommRing`, `LinearOrder` and `IsStrictOrderedRing`.

An example:
```lean
example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0) : False := by
  linarith
```

`linarith` will use all appropriate hypotheses and the negation of the goal, if applicable.
Disequality hypotheses require case splitting and are not normally considered
(see the `splitNe` option below).

`linarith [t1, t2, t3]` will additionally use proof terms `t1, t2, t3`.

`linarith only [h1, h2, h3, t1, t2, t3]` will use only the goal (if relevant), local hypotheses
`h1`, `h2`, `h3`, and proofs `t1`, `t2`, `t3`. It will ignore the rest of the local context.

`linarith!` will use a stronger reducibility setting to try to identify atoms. For example,
```lean
example (x : ℚ) : id x ≥ x := by
  linarith
```
will fail, because `linarith` will not identify `x` and `id x`. `linarith!` will.
This can sometimes be expensive.

`linarith (config := { .. })` takes a config object with five
optional arguments:
* `discharger` specifies a tactic to be used for reducing an algebraic equation in the
  proof stage. The default is `ring`. Other options include `simp` for basic
  problems.
* `transparency` controls how hard `linarith` will try to match atoms to each other. By default
  it will only unfold `reducible` definitions.
* If `splitHypotheses` is true, `linarith` will split conjunctions in the context into separate
  hypotheses.
* If `splitNe` is `true`, `linarith` will case split on disequality hypotheses.
  For a given `x ≠ y` hypothesis, `linarith` is run with both `x < y` and `x > y`,
  and so this runs linarith exponentially many times with respect to the number of
  disequality hypotheses. (`false` by default.)
* If `exfalso` is `false`, `linarith` will fail when the goal is neither an inequality nor `False`.
  (`true` by default.)
* If `minimize` is `false`, `linarith?` will report all hypotheses appearing in its initial
  proof without attempting to drop redundancies. (`true` by default.)
* `restrict_type` (not yet implemented in mathlib4)
  will only use hypotheses that are inequalities over `tp`. This is useful
  if you have e.g. both integer- and rational-valued inequalities in the local context, which can
  sometimes confuse the tactic.

A variant, `nlinarith`, does some basic preprocessing to handle some nonlinear goals.

The option `set_option trace.linarith true` will trace certain intermediate stages of the `linarith`
routine.
 -/
Mathlib.Tactic.linarith : Lean.ParserDescr
-- Mathlib.Algebra.Group.Pi.Basic
Function.extend_add : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Add γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ),
  Function.extend f (g₁ + g₂) (e₁ + e₂) = Function.extend f g₁ e₁ + Function.extend f g₂ e₂
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
isRoot_of_unity_iff : ∀ {n : ℕ},
  0 < n →
    ∀ (R : Type u_2) [inst : CommRing R] [IsDomain R] {ζ : R},
      ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, (Polynomial.cyclotomic i R).IsRoot ζ
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.eq_coe_Ico : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)]
  [Archimedean 𝕜] (a : AddCircle p), ∃ b ∈ Set.Ico 0 p, ↑b = a
-- Mathlib.Order.CompleteLattice.Basic
Monotone.sInf : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : CompleteLattice β] {s : Set (α → β)},
  (∀ f ∈ s, Monotone f) → Monotone (sInf s)
-- Std.Sync.Notify
Std.Notify.Consumer.resolve : {α : Type} → Std.Notify.Consumer α → α → BaseIO Bool
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.of.inj : ∀ {C : Type u} {a a_1 : C}, CategoryTheory.WithInitial.of a = CategoryTheory.WithInitial.of a_1 → a = a_1
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_def' : ∀ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} (ω : E → E →L[𝕜] F)
  (γ : Path a b), curveIntegral ω γ = ∫ (t : ℝ) in 0..1, curveIntegralFun ω γ t
-- Lean.Parser.Command
Lean.Parser.Command.end.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Normed.Group.Uniform
nnnorm_map : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
  [inst_2 : FunLike 𝓕 E F] [IsometryClass 𝓕 E F] [ZeroHomClass 𝓕 E F] (f : 𝓕) (x : E), ‖f x‖₊ = ‖x‖₊
-- Mathlib.Data.Seq.Basic
Stream'.Seq.Pairwise.nil : ∀ {α : Type u} {R : α → α → Prop}, Stream'.Seq.Pairwise R Stream'.Seq.nil