mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Sat.FromLRAT
/-- A (multiple) deletion step, which deletes all the listed clause IDs from the context  -/
Mathlib.Tactic.Sat.LRATStep.del : Array ℕ → Mathlib.Tactic.Sat.LRATStep
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.isPell_one : ∀ {a : ℕ} (a1 : 1 < a), Pell.IsPell { re := ↑a, im := 1 }
-- Mathlib.Data.Nat.Prime.Int
Int.prime_ofNat_iff : ∀ {n : ℕ}, Prime (OfNat.ofNat n) ↔ Nat.Prime (OfNat.ofNat n)
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Under.mapPushoutAdj_counit_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushoutsAlong f] (Y_1 : CategoryTheory.Under Y),
  (CategoryTheory.Under.mapPushoutAdj f).counit.app Y_1 =
    CategoryTheory.Under.homMk
      (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.id Y_1.right) Y_1.hom ⋯) ⋯
-- Std.Time.Date.Basic
Std.Time.instHAddOffset_6 : HAdd Std.Time.Week.Offset Std.Time.Week.Offset Std.Time.Week.Offset
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUInt8HXorOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ^^^ x2) 0
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- The composition of continuous affine maps as a continuous affine map  -/
ContinuousAffineMap.comp : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        {Q : Type u_5} →
          [inst : Ring R] →
            [inst_1 : AddCommGroup V] →
              [inst_2 : Module R V] →
                [inst_3 : TopologicalSpace P] →
                  [inst_4 : AddTorsor V P] →
                    [inst_5 : AddCommGroup W] →
                      [inst_6 : Module R W] →
                        [inst_7 : TopologicalSpace Q] →
                          [inst_8 : AddTorsor W Q] →
                            {W₂ : Type u_6} →
                              {Q₂ : Type u_7} →
                                [inst_9 : AddCommGroup W₂] →
                                  [inst_10 : Module R W₂] →
                                    [inst_11 : TopologicalSpace Q₂] →
                                      [inst_12 : AddTorsor W₂ Q₂] → (Q →ᴬ[R] Q₂) → (P →ᴬ[R] Q) → P →ᴬ[R] Q₂
-- Std.Do.SPred.SPred
_private.Std.Do.SPred.SPred.0.Std.Do.SPred.conjunction.match_1.eq_2 : ∀ {σs : List (Type u_1)} (motive : List (Std.Do.SPred σs) → Sort u_2) (P : Std.Do.SPred σs)
  (env : List (Std.Do.SPred σs)) (h_1 : Unit → motive [])
  (h_2 : (P : Std.Do.SPred σs) → (env : List (Std.Do.SPred σs)) → motive (P :: env)),
  (match P :: env with
    | [] => h_1 ()
    | P :: env => h_2 P env) =
    h_2 P env
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
OrderIso.mulLeft₀_apply : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [inst_2 : PosMulReflectLT G₀] (a : G₀)
  (ha : 0 < a) (x : G₀), (OrderIso.mulLeft₀ a ha) x = a * x
-- Mathlib.Algebra.Order.Quantale
AddQuantale.instAddLeftMono : ∀ {α : Type u_1} [inst : AddSemigroup α] [inst_1 : CompleteLattice α] [IsAddQuantale α], AddLeftMono α
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.mk.inj : ∀ {X : Type u_5} {Y : Type u_6} {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y} {toEquiv : X ≃ Y}
  {continuous_toFun : autoParam (Continuous toEquiv.toFun) Homeomorph.continuous_toFun._autoParam}
  {continuous_invFun : autoParam (Continuous toEquiv.invFun) Homeomorph.continuous_invFun._autoParam}
  {toEquiv_1 : X ≃ Y}
  {continuous_toFun_1 : autoParam (Continuous toEquiv_1.toFun) Homeomorph.continuous_toFun._autoParam}
  {continuous_invFun_1 : autoParam (Continuous toEquiv_1.invFun) Homeomorph.continuous_invFun._autoParam},
  { toEquiv := toEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
      { toEquiv := toEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 } →
    toEquiv = toEquiv_1
-- Mathlib.Algebra.GroupWithZero.Basic
zpow_add₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (m n : ℤ), a ^ (m + n) = a ^ m * a ^ n
-- Mathlib.Order.Disjointed
disjointed_subset : ∀ {α : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι] (f : ι → Set α) (i : ι),
  disjointed f i ⊆ f i
-- Mathlib.Algebra.Order.GroupWithZero.Basic
le_mul_of_one_le_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [MulPosMono α],
  0 ≤ b → 1 ≤ a → b ≤ a * b
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_intCast_sub : ∀ {x : ℝ} (m : ℤ), Irrational (↑m - x) → Irrational x
-- Qq.Match
Qq.Impl.term_comefrom_Do_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y : C} [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {J : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (CategoryTheory.MonoOver Y))
  (c : CategoryTheory.Limits.Cocone F),
  CategoryTheory.CommSq (CategoryTheory.Limits.Sigma.desc fun i => CategoryTheory.Over.Hom.left (c.ι.app i).hom)
    (CategoryTheory.MonoOver.strongEpiMonoFactorisationSigmaDesc F).e c.pt.arrow
    (CategoryTheory.MonoOver.strongEpiMonoFactorisationSigmaDesc F).m
-- Mathlib.LinearAlgebra.Quotient.Defs
/-- Quotienting by equal submodules gives linearly equivalent quotients.  -/
Submodule.quotEquivOfEq : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (p p' : Submodule R M) → p = p' → (M ⧸ p) ≃ₗ[R] M ⧸ p'
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.paren.inj : ∀ {ref : Lean.Syntax} {a : Lean.Elab.Tactic.RCases.RCasesPatt} {ref_1 : Lean.Syntax}
  {a_1 : Lean.Elab.Tactic.RCases.RCasesPatt},
  Lean.Elab.Tactic.RCases.RCasesPatt.paren ref a = Lean.Elab.Tactic.RCases.RCasesPatt.paren ref_1 a_1 →
    ref = ref_1 ∧ a = a_1
-- Mathlib.Topology.Path
Path.continuous : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), Continuous ⇑γ
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.truncGE.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K K_1 : HomologicalComplex C c') (e_K : K = K_1) (e e_1 : c.Embedding c') (e_e : e = e_1) [inst_2 : e.IsTruncGE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : CategoryTheory.Limits.HasZeroObject C],
  K.truncGE e = K_1.truncGE e_1
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `i` is an `F`-algebra isomorphism of `E` and `K`, then the image of `perfectClosure F E`
under the map `i` is equal to in `perfectClosure F K`.  -/
perfectClosure.map_eq_of_algEquiv : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E ≃ₐ[F] K), IntermediateField.map (↑i) (perfectClosure F E) = perfectClosure F K
-- Init.Data.Range.Polymorphic.RangeIterator
Std.IteratorLoop.rel.eq_1 : ∀ (α : Type w) (m : Type w → Type w') {β : Type w} [inst : Std.Iterator α m β] {γ : Type x}
  (plausible_forInStep : β → γ → ForInStep γ → Prop) (p' p : Std.IterM m β × γ),
  Std.IteratorLoop.rel α m plausible_forInStep p' p =
    ((∃ b, p.1.IsPlausibleStep (Std.IterStep.yield p'.1 b) ∧ plausible_forInStep b p.2 (ForInStep.yield p'.2)) ∨
      p.1.IsPlausibleStep (Std.IterStep.skip p'.1) ∧ p'.2 = p.2)
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.coeff_smul : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : SMulZeroClass S R] {n : ℕ} {a : S} {f : Polynomial R},
  (a • f).coeff n = a • f.coeff n
-- Mathlib.Topology.Algebra.Module.LocallyConvex
LocallyConvexSpace.mk : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E],
  (∀ (x : E), (nhds x).HasBasis (fun s => s ∈ nhds x ∧ Convex 𝕜 s) id) → LocallyConvexSpace 𝕜 E
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- An auxiliary lemma for the proof of `AffineIndependent.vectorSpan_image_eq_iff`.  -/
_private.Mathlib.LinearAlgebra.AffineSpace.Independent.0.AffineIndependent.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P},
  AffineIndependent k p →
    ∀ {s₁ s₂ : Set ι} {i : ι}, i ∈ s₁ → i ∉ s₂ → ¬s₁.Subsingleton → vectorSpan k (p '' s₁) ≠ vectorSpan k (p '' s₂)
-- Mathlib.Algebra.Central.TensorProduct
/-- Let `B` and `C` be two algebras over a field `K`, if `B ⊗[K] C` is central and `B` is
non-trivial, then `C` is central.  -/
Algebra.IsCentral.right_of_tensor_of_field : ∀ (K : Type u_4) (B : Type u_5) (C : Type u_6) [inst : Field K] [inst_1 : Ring B] [inst_2 : Ring C] [Nontrivial B]
  [inst_4 : Algebra K B] [inst_5 : Algebra K C] [Algebra.IsCentral K (TensorProduct K B C)], Algebra.IsCentral K C
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.h : {A : Type u} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          (self : Algebra.Smooth.DescentAux✝ A B) →
            Algebra.Smooth.DescentAux.vars✝ self → MvPolynomial (Algebra.Smooth.DescentAux.vars✝ self) A
-- Mathlib.GroupTheory.OrderOfElement
AddLeftCancelMonoid.addGroupOfFinite.eq_1 : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] [inst_1 : Finite G],
  AddLeftCancelMonoid.addGroupOfFinite =
    { toAddMonoid := inst.toAddMonoid, neg := fun x => (addOrderOf x - 1) • x, sub := SubNegMonoid.sub',
      zsmul := zsmulRec, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.Data.PNat.Xgcd
/-- `zp` is a variable which changes through the algorithm.  -/
PNat.XgcdType.zp : PNat.XgcdType → ℕ
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.finitaryExtensive_of_preserves_and_reflects : ∀ {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.FinitaryExtensive D]
  [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.HasPullbacksOfInclusions C]
  [CategoryTheory.PreservesPullbacksOfInclusions F]
  [CategoryTheory.Limits.ReflectsLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  [CategoryTheory.Limits.ReflectsColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F],
  CategoryTheory.FinitaryExtensive C
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_tmul : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) (m : M) (n : N),
  (TensorProduct.map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R₂] g n
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
_private.Mathlib.GroupTheory.SpecificGroups.Dihedral.0.instDecidableEqDihedralGroup.decEq.match_1.eq_1 : ∀ {n : ℕ} (motive : DihedralGroup n → DihedralGroup n → Sort u_1) (a b : ZMod n)
  (h_1 : (a b : ZMod n) → motive (DihedralGroup.r a) (DihedralGroup.r b))
  (h_2 : (a a_1 : ZMod n) → motive (DihedralGroup.r a) (DihedralGroup.sr a_1))
  (h_3 : (a a_1 : ZMod n) → motive (DihedralGroup.sr a) (DihedralGroup.r a_1))
  (h_4 : (a b : ZMod n) → motive (DihedralGroup.sr a) (DihedralGroup.sr b)),
  (match DihedralGroup.r a, DihedralGroup.r b with
    | DihedralGroup.r a, DihedralGroup.r b => h_1 a b
    | DihedralGroup.r a, DihedralGroup.sr a_1 => h_2 a a_1
    | DihedralGroup.sr a, DihedralGroup.r a_1 => h_3 a a_1
    | DihedralGroup.sr a, DihedralGroup.sr b => h_4 a b) =
    h_1 a b
-- Mathlib.Data.Fintype.EquivFin
Equiv.ofRightInverseOfCardLE_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (hαβ : Fintype.card α ≤ Fintype.card β)
  (f : α → β) (g : β → α) (h : Function.RightInverse g f) (a : β), (Equiv.ofRightInverseOfCardLE hαβ f g h).symm a = g a
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.trailingDegree 0 = ⊤
-- Mathlib.Algebra.Group.End
Equiv.Perm.extendDomain_zpow : ∀ {α : Type u_4} {β : Type u_5} (e : Equiv.Perm α) {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p) (n : ℤ),
  (e ^ n).extendDomain f = e.extendDomain f ^ n
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.id_mapComp_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  ((CategoryTheory.StrictPseudofunctor.id B).mapComp f g).inv =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.prop.arrowIso_inv_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C}
  {f : X ⟶ Y} (hf : Φ.prop f), hf.arrowIso.inv.right = CategoryTheory.eqToHom ⋯
-- Mathlib.Order.SetNotation
/-- Infimum of a set  -/
InfSet.sInf : {α : Type u_1} → [self : InfSet α] → Set α → α
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.vadd_def : ∀ {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [inst : (i : ι) → VAdd α (M i)] (a : α) (f : (i : ι) → M i),
  a +ᵥ f = fun i => a +ᵥ f i
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
tendstoLocallyUniformlyOn_TFAE : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {s : Set α}
  [LocallyCompactSpace α] (G : ι → α → β) (g : α → β) (p : Filter ι),
  IsOpen s →
    [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K,
        ∀ x ∈ s, ∃ v ∈ nhdsWithin x s, TendstoUniformlyOn G g p v].TFAE
-- Plausible.Sampleable
/-- An annotation for values that should never get shrunk.  -/
Plausible.NoShrink : Type u → Type u
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
/-- To check that `f` is bounded at `c`, it suffices for `f ∣[k] g` to be bounded at `∞` for any
single `g` with `g • ∞ = c`.  -/
OnePoint.isBoundedAt_iff : ∀ {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} {g : GL (Fin 2) ℝ},
  g • OnePoint.infty = c → (c.IsBoundedAt f k ↔ UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k g f))
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.measurableSet_iSup : ∀ {α : Type u_1} {ι : Sort u_7} {m : ι → MeasurableSpace α} {s : Set α},
  MeasurableSet s ↔ MeasurableSpace.GenerateMeasurable {s | ∃ i, MeasurableSet s} s
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
/-- If `Q` contains identities and respects isomorphisms (i.e. is satisfied by isomorphisms),
and `P` is affine locally defined by `affineAnd Q`, then `P` contains identities.  -/
AlgebraicGeometry.HasAffineProperty.affineAnd_containsIdentities : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
  AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
      (RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q) → P.ContainsIdentities
-- Mathlib.Data.Int.Interval
Int.card_Ioc_of_le : ∀ (a b : ℤ), a ≤ b → ↑(Finset.Ioc a b).card = b - a
-- Std.Async.Select
/-- The event source.
 -/
Std.Async.Selectable.selector : {α : Type} → (self : Std.Async.Selectable α) → Std.Async.Selector self.β
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.coe_add : ∀ {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]
  (D1 D2 : LieDerivation R L M), ⇑(D1 + D2) = ⇑D1 + ⇑D2
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- The quadratic form sending elements to the negation of their square.  -/
CliffordAlgebraComplex.Q : QuadraticForm ℝ ℝ
-- 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.tacticLinarith!_ : Lean.ParserDescr
-- Mathlib.Data.Fin.Fin2
Fin2.castSucc.eq_def : ∀ {n : ℕ} (x : Fin2 n),
  x.castSucc =
    match n, x with
    | .(n + 1), Fin2.fz => Fin2.fz
    | .(n + 1), k.fs => k.castSucc.fs
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.neg_add_cancel_assoc : ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → -a + (b + a) = b
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.add_sum_Ioi_eq_sum_Ici : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → M} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrderTop α] (a : α), f a + ∑ x > a, f x = ∑ x ≥ a, f x
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.image_apply_finMulAntidiag : ∀ {d n : ℕ} {i : Fin d}, d ≠ 1 → Finset.image (fun f => f i) (d.finMulAntidiag n) = n.divisors
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec : (R : CommRingCat) → [inst : IsDomain ↑R] → Algebra ↑R ↑(AlgebraicGeometry.Spec R).functionField
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.isMinOn_T_real : ∀ {n k : ℕ},
  n ≠ 0 →
    k ≤ n →
      Odd k →
        IsMinOn (fun x => Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n)) (Set.Icc (-1) 1)
          (Real.cos (↑k * Real.pi / ↑n))
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.eq' : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} {f g : ↥(MeasureTheory.Lp.simpleFunc E p μ)}, ↑↑f = ↑↑g → f = g
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring contains the ring's 1.  -/
Subring.one_mem : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R), 1 ∈ s
-- Mathlib.Order.SetAccumulate
Set.accumulate_def : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : LE α] {x : α}, Set.accumulate s x = ⋃ y, ⋃ (_ : y ≤ x), s y
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- Eta-expanded form of `Meromorphic.logDeriv_mul_eventuallyEq`

---

The logarithmic derivative converts products into sums: away from a codiscrete subset of `𝕜`, the
logarithmic derivative of a product of two meromorphic functions is the sum of the logarithmic
derivatives.
 -/
Meromorphic.logDeriv_fun_mul_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'},
  Meromorphic f →
    Meromorphic g →
      (∀ (x : 𝕜), meromorphicOrderAt f x ≠ ⊤) →
        (∀ (x : 𝕜), meromorphicOrderAt g x ≠ ⊤) →
          (logDeriv fun i => f i * g i) =ᶠ[Filter.codiscrete 𝕜] fun i => logDeriv f i + logDeriv g i
-- Mathlib.RingTheory.LocalIso
Algebra.IsLocalIso.of_algEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {T : Type u_3}
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T) [Algebra.IsLocalIso R S], Algebra.IsLocalIso R T
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Box.splitLower_le : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ}, I.splitLower i x ≤ ↑I
-- Init.Data.SInt.Float
/-- Obtains the `Float` whose value is the same as the given `Int32`.

This function does not reduce in the kernel.
 -/
Int32.toFloat : Int32 → Float
-- Mathlib.FieldTheory.IntermediateField.Algebraic
/-- Mapping a finite-dimensional intermediate field along an algebra equivalence gives
a finite-dimensional intermediate field.  -/
IntermediateField.finiteDimensional_map : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {E : IntermediateField K L}
  (f : L →ₐ[K] L) [FiniteDimensional K ↥E], FiniteDimensional K ↥(IntermediateField.map f E)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- `LinearMap.rTensor` as a continuous linear map, i.e. the continuous linear map `f` extended to
the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] y`.  -/
ContinuousLinearMap.rTensor : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      (G : Type u_4) →
        [inst : RCLike 𝕜] →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : InnerProductSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : InnerProductSpace 𝕜 F] →
                  [inst_5 : NormedAddCommGroup G] →
                    [inst_6 : InnerProductSpace 𝕜 G] → (E →L[𝕜] F) → TensorProduct 𝕜 E G →L[𝕜] TensorProduct 𝕜 F G
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The fully faithful embedding of `LightProfinite` in `TopCat`.
This is definitionally the same as the obvious composite.  -/
LightProfinite.toTopCat : CategoryTheory.Functor LightProfinite TopCat