mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- There is some classifier.  -/
CategoryTheory.HasSubobjectClassifier.exists_classifier : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.HasSubobjectClassifier C],
  Nonempty (CategoryTheory.Subobject.Classifier C)
-- Lean.Meta.TransparencyMode
Lean.Meta.TransparencyMode.instToString_lean : ToString Lean.Meta.TransparencyMode
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.instGeometricallyConnectedFiberToSpecResidueField : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (s : ↥S) [AlgebraicGeometry.GeometricallyConnected f],
  AlgebraicGeometry.GeometricallyConnected (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f s)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.equiv_iff_toArray_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ t₁.toArray = t₂.toArray)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- Adding a zeroth term to a formal multilinear series taking values in `E →L[𝕜] F`. This
corresponds to starting from a Taylor series (`HasFTaylorSeriesUpTo`) for the derivative of a
function, and building a Taylor series for the function itself.  -/
FormalMultilinearSeries.unshift : {𝕜 : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F) → F → FormalMultilinearSeries 𝕜 E F
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- Neutral element for multiplication.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.one : {basis : Tactic.ComputeAsymptotics.Basis} → Tactic.ComputeAsymptotics.MultiseriesExpansion basis
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.map_map : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] {M'' : Type u_6} {N'' : Type u_7} [inst_4 : MulOneClass M'']
  [inst_5 : MulOneClass N''] (f' : M' →* M'') (g' : N' →* N'') (f : M →* M') (g : N →* N') (x : Monoid.Coprod M N),
  (Monoid.Coprod.map f' g') ((Monoid.Coprod.map f g) x) = (Monoid.Coprod.map (f'.comp f) (g'.comp g)) x
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqArg.beq : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Arg pu → Lean.Compiler.LCNF.Arg pu → Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_append_of_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l' = false →
    Std.Internal.List.getValueCast? a (l ++ l') = Std.Internal.List.getValueCast? a l
-- Init.Data.Rat.Lemmas
Rat.num_pow : ∀ (q : ℚ) (n : ℕ), (q ^ n).num = q.num ^ n
-- Mathlib.Algebra.Algebra.Pi
Pi.constAlgHom_apply : ∀ (R : Type u_2) [inst : CommSemiring R] (A : Type u_5) (B : Type u_6) [inst_1 : Semiring B] [inst_2 : Algebra R B]
  (a : B) (a_1 : A), (Pi.constAlgHom R A B) a a_1 = Function.const A a a_1
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
/-- The map-structural characterisation of pivots. This is useful for proving that
a matrix is in row echelon form.  -/
Matrix.isPivotedBy_iff : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Zero R] {A : Matrix m n R} {l : m → WithTop n}
  [inst_1 : PartialOrder m] [inst_2 : LinearOrder n],
  A.IsPivotedBy l ↔
    Monotone l ∧
      StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
-- Init.Data.Int.Order
Int.add_le_add_three : ∀ {a b c d e f : ℤ}, a ≤ d → b ≤ e → c ≤ f → a + b + c ≤ d + e + f
-- Std.Data.DHashMap.Internal.Defs
Std.DHashMap.Internal.IsHashSelf.mk : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Array (Std.DHashMap.Internal.AssocList α β)},
  (∀ (i : ℕ) (h : i < m.size), Std.DHashMap.Internal.List.HashesTo m[i].toList i m.size) →
    Std.DHashMap.Internal.IsHashSelf m
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) (b : (F.obj A.obj).obj),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.PreGaloisCategory.autIsoFibers F).inv.app A)) b =
    (CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois F A.obj A.pt).symm b
-- Lean.Meta.AppBuilder
/-- Given `h : a ≍ b`, returns a proof of `b ≍ a`.   -/
Lean.Meta.mkHEqSymm : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.toOne : {E : Type u_3} → [inst : Group E] → [DecidableEq E] → One (GroupNorm E)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Non-dependent recursion principle for localizations: given elements `f x y : p`
for all `x` and `y`, such that `r S x x'` and `r S y y'` implies `f x y = f x' y'`,
then `f` is defined on the whole `Localization S`.  -/
Localization.liftOn₂ : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {p : Sort u} →
        Localization S →
          Localization S →
            (f : M → ↥S → M → ↥S → p) →
              (∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
                  (Localization.r S) (a, b) (a', b') → (Localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d') →
                p
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.leftUnitor_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Lax.OplaxTrans.leftUnitor η).hom.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom
-- Mathlib.Data.Fin.Basic
Fin.equivSubtype_apply : ∀ {n : ℕ} (a : Fin n), Fin.equivSubtype a = ⟨↑a, ⋯⟩
-- Lean.Environment
_private.Lean.Environment.0.Lean.Kernel.Environment.mk.injEq : ∀ (constants : Lean.ConstMap) (quotInit : Bool) (diagnostics : Lean.Kernel.Diagnostics)
  (const2ModIdx : Std.HashMap Lean.Name Lean.ModuleIdx) (extensions irBaseExts : Array Lean.EnvExtensionState)
  (header : Lean.EnvironmentHeader) (constants_1 : Lean.ConstMap) (quotInit_1 : Bool)
  (diagnostics_1 : Lean.Kernel.Diagnostics) (const2ModIdx_1 : Std.HashMap Lean.Name Lean.ModuleIdx)
  (extensions_1 irBaseExts_1 : Array Lean.EnvExtensionState) (header_1 : Lean.EnvironmentHeader),
  ({ constants := constants, quotInit := quotInit, diagnostics := diagnostics, const2ModIdx := const2ModIdx,
        extensions := extensions, irBaseExts := irBaseExts, header := header } =
      { constants := constants_1, quotInit := quotInit_1, diagnostics := diagnostics_1, const2ModIdx := const2ModIdx_1,
        extensions := extensions_1, irBaseExts := irBaseExts_1, header := header_1 }) =
    (constants = constants_1 ∧
      quotInit = quotInit_1 ∧
        diagnostics = diagnostics_1 ∧
          const2ModIdx = const2ModIdx_1 ∧ extensions = extensions_1 ∧ irBaseExts = irBaseExts_1 ∧ header = header_1)
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.norm_bilinearRestrictScalars : ∀ {𝕜 : Type u_1} {E : Type u_4} {F : Type u_6} {G : Type u_8} {𝕜' : Type u_11} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] [inst_3 : SeminormedAddCommGroup E]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E]
  [inst_7 : SeminormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F]
  [inst_10 : IsScalarTower 𝕜 𝕜' F] [inst_11 : SeminormedAddCommGroup G] [inst_12 : NormedSpace 𝕜 G]
  [inst_13 : NormedSpace 𝕜' G] [inst_14 : IsScalarTower 𝕜 𝕜' G] (B : E →L[𝕜'] F →L[𝕜'] G),
  ‖ContinuousLinearMap.bilinearRestrictScalars 𝕜 B‖ = ‖B‖
-- Init.Data.List.Lemmas
List.forall_mem_filter : ∀ {α : Type u_1} {l : List α} {p : α → Bool} {P : α → Prop}, (∀ i ∈ List.filter p l, P i) ↔ ∀ j ∈ l, p j = true → P j
-- Mathlib.Algebra.Order.Star.Conjneg
conjneg_pos : ∀ {G : Type u_1} {R : Type u_2} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : PartialOrder R]
  [inst_3 : StarRing R] [StarOrderedRing R] {f : G → R}, 0 < conjneg f ↔ 0 < f
-- Mathlib.LinearAlgebra.Matrix.DotProduct
dotProduct_eq_iff : ∀ {n : Type u_2} {R : Type u_4} [inst : Semiring R] [inst_1 : Fintype n] {v w : n → R},
  (∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u) ↔ v = w
-- Mathlib.Tactic.ClickSuggestions.Apply
Mathlib.Tactic.ClickSuggestions.ApplyLemma.mk.sizeOf_spec : ∀ (name : Mathlib.Tactic.ClickSuggestions.Premise), sizeOf { name := name } = 1 + sizeOf name
-- Mathlib.Algebra.Order.IsBotOne
eq_zero_or_pos : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α] (a : α), a = 0 ∨ 0 < a
-- Mathlib.Data.List.Lemmas
List.injOn_insertIdx_index_of_notMem : ∀ {α : Type u_1} (l : List α), ∀ x ∉ l, Set.InjOn (fun k => l.insertIdx k x) {n | n ≤ l.length}
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- The category instance on `CatEnriched C` promotes it to a `Cat` enriched ordinary
category.  -/
CategoryTheory.CatEnriched.instEnrichedOrdinaryCategoryCat : {C : Type u_1} →
  [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] →
    CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat (CategoryTheory.CatEnriched C)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_associator_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {l₁ : a ⟶ b} {r₁ : b ⟶ a}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) {l₂ : b ⟶ c} {r₂ : c ⟶ b}
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) {l₃ : c ⟶ d} {r₃ : d ⟶ c}
  (adj₃ : CategoryTheory.Bicategory.Adjunction l₃ r₃),
  (CategoryTheory.Bicategory.conjugateEquiv (adj₁.comp (adj₂.comp adj₃)) ((adj₁.comp adj₂).comp adj₃))
      (CategoryTheory.Bicategory.associator l₁ l₂ l₃).hom =
    (CategoryTheory.Bicategory.associator r₃ r₂ r₁).hom
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : Module.Free R V] [inst_4 : Module.Finite R V] (r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)),
  ↑↑↑(SpecialLinearGroup.centerEquivRootsOfUnity.symm r) = r • LinearMap.id
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- Any functor between Cartesian-monoidal categories is oplax monoidal.

This is not made an instance because it would create a diamond for the oplax monoidal structure on
the identity and composition of functors.  -/
CategoryTheory.Functor.OplaxMonoidal.ofChosenFiniteProducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] → (F : CategoryTheory.Functor C D) → F.OplaxMonoidal
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_pullback_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y : C) {X_1 Y_1 : CategoryTheory.Over X} (g : X_1 ⟶ Y_1),
  (CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)).map g =
    CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Over.Hom.left g) Y) ⋯
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.step_filterM : ∀ {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  {f : β → n (ULift.{w, 0} Bool)} [inst_1 : Monad n] [inst_2 : MonadAttach n] [LawfulMonad n] [inst_4 : MonadLiftT m n],
  (Std.IterM.filterM f it).step = do
    let __do_lift ← liftM it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => do
        let __do_lift ← MonadAttach.attach (f out)
        match __do_lift with
          | ⟨{ down := false }, hf⟩ =>
            pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.filterM f it') ⋯))
          | ⟨{ down := true }, hf⟩ =>
            pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.filterM f it') out ⋯))
      | ⟨Std.IterStep.skip it', h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.filterM f it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Std.Time.Zoned.RecurringRule
/-- A single DST transition rule: a date specification and a wall-clock time.
 -/
Std.Time.TimeZone.TransitionRule : Type
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalClosure.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G),
  AddSubgroup.normalClosure s = AddSubgroup.closure (AddGroup.addConjugatesOfSet s)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.of_adj : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), h.toWalk.IsPath
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.self_sub_floor_lt_one : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R] (a : R),
  a - ↑⌊a⌋₊ < 1
-- Std.Data.TreeMap.Basic
/-- Carries out a monadic action on each mapping in the tree map in ascending order.  -/
Std.TreeMap.forM : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {m : Type w → Type w₂} → [Monad m] → (α → β → m PUnit.{w + 1}) → Std.TreeMap α β cmp → m PUnit.{w + 1}
-- Lean.Meta.Tactic.Grind.Core
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.addEqCore : Lean.Expr → Lean.Expr → Lean.Expr → Bool → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.single_obj_X_self : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : V), ((HomologicalComplex.single V c j).obj A).X j = A
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_subset : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (id : ℕ), ∀ c ∈ (f.deleteOne id).toList, c ∈ f.toList
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Tactic.ComputeAsymptotics.Majorized.mul_bounded : ∀ {f g basis_hd : ℝ → ℝ} {exp : ℝ},
  Tactic.ComputeAsymptotics.Majorized f basis_hd exp →
    (g =O[Filter.atTop] fun x => 1) → Tactic.ComputeAsymptotics.Majorized (f * g) basis_hd exp
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
tangentMap_prod_left : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {p : TangentBundle I M} {y₀ : M'},
  tangentMap I (I.prod I') (fun x => (x, y₀)) p = ⟨(p.proj, y₀), (p.snd, 0)⟩
-- Mathlib.Data.List.Map2
List.nil_zipWith : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (l : List β), List.zipWith f [] l = []
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.get : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [LawfulBEq α] → [inst_2 : Hashable α] → (m : Std.DHashMap.Internal.Raw₀ α β) → (a : α) → m.contains a = true → β a
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.fixupInline.getCustom : Lean.ElabInline → Option Dynamic
-- Mathlib.CategoryTheory.Types.Basic
/-- Typecheck a function as a morphism in `Type`.  -/
CategoryTheory.«term↾_» : Lean.ParserDescr
-- Mathlib.Order.SuccPred.Limit
Order.not_isPredPrelimit_of_noMin : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : PredOrder α] [IsPredArchimedean α] [NoMinOrder α] [NoMaxOrder α],
  ¬Order.IsPredPrelimit a
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instIsTopologicalAddGroupCarrier : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] (M : TopModuleCat R), IsTopologicalAddGroup ↑M.toModuleCat
-- Mathlib.Order.BooleanAlgebra.Set
Set.inter_eq_compl_compl_union_compl : ∀ {α : Type u_1} (s t : Set α), s ∩ t = (sᶜ ∪ tᶜ)ᶜ
-- Mathlib.Data.Finset.Sigma
Finset.sigma_eq_biUnion : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ((i : ι) × α i)] (s : Finset ι) (t : (i : ι) → Finset (α i)),
  s.sigma t = s.biUnion fun i => Finset.map (Function.Embedding.sigmaMk i) (t i)
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.isCompl_genWeightSpaceOf_zero_posFittingCompOf : ∀ (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] [IsNoetherian R M] [IsArtinian R M] (x : L),
  IsCompl (LieModule.genWeightSpaceOf M 0 x) (LieModule.posFittingCompOf R M x)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.instZeroOfNontrivial : {R : Type r} → [inst : CommRing R] → {W' : WeierstrassCurve.Projective R} → [Nontrivial R] → Zero W'.Point
-- Mathlib.Algebra.GroupWithZero.Defs
IsCancelMulZero.toIsRightCancelMulZero : ∀ {M₀ : Type u} {inst : Mul M₀} {inst_1 : Zero M₀} [self : IsCancelMulZero M₀], IsRightCancelMulZero M₀
-- Init.SimpLemmas
and_congr_right_iff : ∀ {a b c : Prop}, (a ∧ b ↔ a ∧ c) ↔ a → (b ↔ c)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited γ] {f : α → β → Option γ} {k : α},
  (Std.TreeMap.filterMap f t)[k]! = (t[k]?.pbind fun x h' => f (t.getKey k ⋯) x).get!
-- Mathlib.Tactic.FieldSimp.Discharger
/-- Default discharge strategy for `field` and `field_simp`: try to solve the (in)equality `prop`,
of the form `t = 0` or `t > 0`, by one of the following strategies:

* Use an assumption from the context.
* Use the `norm_num` tactic.
* Use the `positivity` tactic.
* Use the `simp` tactic with `discharge` as discharger and lemmas stating:
  * `2 ≠ 0`, `3 ≠ 0`, `4 ≠ 0`
  * `x ≠ 0 → y ≠ 0 → x * y ≠ 0`
  * `a ≠ 0 → a ^ n ≠ 0` (for `n : ℕ` and `n : ℤ`)
  * `↑n + 1 ≠ 0`, if `n : ℕ` and the field has characteristic 0.

If none of the strategies finds a proof for `prop`, the result is `none`.
 -/
Mathlib.Tactic.FieldSimp.discharge : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)
-- Qq.ForLean.Do
Lean.Elab.Term.mkIdBindFor : Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Term.ExtractMonadResult
-- Mathlib.Order.LiminfLimsup
Filter.limsup_iInf_le_iInf_limsup : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : CompleteLattice α] {f : Filter β} {u : ι → β → α},
  Filter.limsup (fun b => ⨅ i, u i b) f ≤ ⨅ i, Filter.limsup (u i) f
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.toStructuredArrow_comp_proj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F),
  c.toStructuredArrow.comp (CategoryTheory.StructuredArrow.proj c.pt F) = CategoryTheory.Functor.id J
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.finitary : ∀ {α : Type u_1} {N M : Matroid α} [M.Finitary], N.IsRestriction M → N.Finitary
-- Mathlib.Tactic.Field
/-- `field` solves equality goals in (semi-)fields. The goal must be an equality which is *universal*,
in the sense that it is true in any field in which the appropriate denominators don't vanish.
(That is, it is a consequence purely of the field axioms.)

The `field` tactic is built from the tactics `field_simp` (which clears the denominators) and `ring`
(which proves equality goals universally true in commutative (semi-)rings). If `field` fails to
prove your goal, you may still be able to prove your goal by running the `field_simp` and `ring_nf`
normalizations in some order.

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging
fails. These denominators are made out of denominators appearing in the input expression, by
repeatedly taking products or divisors. The default discharger can be non-universal, i.e. can be
specific to the field at hand (order properties, explicit `≠ 0` hypotheses, `CharZero` if that is
known, etc). See `Mathlib.Tactic.FieldSimp.discharge` for full details of the default discharger
algorithm.

* `field (disch := tac)` uses the tactic sequence `tac` to discharge nonzeroness proofs.
* `field [t₁, ..., tₙ]` provides terms `t₁`, ..., `tₙ` to the discharger for nonzeroness proofs.

Examples:
```
example {x y : ℚ} (hx : x + y ≠ 0) : x / (x + y) + y / (x + y) = 1 := by field
example {a b : ℝ} (ha : a ≠ 0) : a / (a * b) - 1 / b = 0 := by field

-- The user can also provide additional terms to help with nonzeroness proofs:
example {K : Type*} [Field K] (hK : ∀ x : K, x ^ 2 + 1 ≠ 0) (x : K) :
    1 / (x ^ 2 + 1) + x ^ 2 / (x ^ 2 + 1) = 1 := by
  field [hK]

example {a b : ℚ} (H : b + a ≠ 0) : a / (a + b) + b / (b + a) = 1 := by
  -- `field` cannot prove this on its own.
  fail_if_success field
  -- But running `ring_nf` and `field_simp` in a different order works:
  ring_nf at *
  field
```

 -/
Mathlib.Tactic.FieldSimp.field : Lean.ParserDescr
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.insertIdx.eq_1 : ∀ {α : Type u} (as : Array α) (i : ℕ) (a : α) (x : i ≤ as.size),
  as.insertIdx i a x = Array.insertIdx.loop✝ i (as.push a) ⟨as.size, ⋯⟩
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.inv_smul_finset_distrib : ∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] (a : α) (s : Finset α), (a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.MorphismProperty.cokernels.of_isColimit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W : CategoryTheory.MorphismProperty C} {X₁ X₂ : C} (f : X₁ ⟶ X₂) (k : CategoryTheory.Limits.CokernelCofork f)
  (hk : CategoryTheory.Limits.IsColimit k), W f → W.cokernels k.pt
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.processPending : Array Lean.MVarId → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
FGAlgCatSkeleton.mk : {R : Type u} → [inst : CommRing R] → (n : ℕ) → Ideal (MvPolynomial (Fin n) R) → FGAlgCatSkeleton R
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Homotopy group of finite index, denoted as `π_n` within the Topology namespace.  -/
Topology.termπ_ : Lean.ParserDescr
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.symm_symm : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁), F.symm.symm = F
-- Batteries.Recycling.RBTree.Lemmas
/-- A "representable cut" is one generated by `cmp a` for some `a`. This is always a valid cut.  -/
RBTree.RBMap.instIsStrictCut : ∀ {α : Type u_1} (cmp : α → α → Ordering) (a : α), RBTree.RBNode.IsStrictCut cmp (cmp a)
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
NonarchimedeanAddGroup.is_nonarchimedean : ∀ {G : Type u_1} {inst : AddGroup G} {inst_1 : TopologicalSpace G} [self : NonarchimedeanAddGroup G],
  ∀ U ∈ nhds 0, ∃ V, ↑V ⊆ U
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.all_eq_false_iff_exists_mem_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  {p : α → β → Bool}, m.all p = false ↔ ∃ a, ∃ (h : a ∈ m), p a (Std.DHashMap.Const.get m a h) = false