mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go.match_4.congr_eq_8 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (a b : Lean.Grind.CommRing.Expr),
  x = a.sub b →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.natCast k => h_2 k
      | Lean.Grind.CommRing.Expr.intCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_8 a b
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHint : Type
-- Mathlib.Order.RelIso.Basic
RelEmbedding.isStrictOrder : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (x : r ↪r s) [IsStrictOrder β s],
  IsStrictOrder α r
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.think_congr : ∀ {α : Type u} {s t : Stream'.WSeq α}, s ~ʷ t → s.think ~ʷ t.think
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableOn.sub_iff_left` -/
DifferentiableOn.fun_sub_iff_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {s : Set E}, DifferentiableOn 𝕜 g s → (DifferentiableOn 𝕜 (fun i => f i - g i) s ↔ DifferentiableOn 𝕜 f s)
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.norm_star : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (x : QuadraticAlgebra R a b),
  QuadraticAlgebra.norm (star x) = QuadraticAlgebra.norm x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicones.functoriality_obj_fst : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (P Q : C) (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms]
  (A : CategoryTheory.Limits.BinaryBicone P Q),
  ((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).fst = F.map A.fst
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
/-- The localization functor `CochainComplex.Plus C ⥤ DerivedCategory.Plus C`.  -/
DerivedCategory.Plus.Q : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → CategoryTheory.Functor (CochainComplex.Plus C) (DerivedCategory.Plus C)
-- Lean.Exception
/-- Similar to `AddMessageContext`, but for error messages.
The default instance just uses `AddMessageContext`.
In error messages, we may want to provide additional information (e.g., macro expansion stack),
and refine the `(ref : Syntax)`.  -/
Lean.AddErrorMessageContext : (Type → Type) → Type
-- Mathlib.MeasureTheory.Measure.Restrict
/-- This lemma shows that `Inf` and `restrict` commute for measures.  -/
MeasureTheory.Measure.restrict_sInf_eq_sInf_restrict : ∀ {α : Type u_2} {t : Set α} {m0 : MeasurableSpace α} {m : Set (MeasureTheory.Measure α)},
  m.Nonempty → MeasurableSet t → (sInf m).restrict t = sInf ((fun μ => μ.restrict t) '' m)
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.instIsDiscreteValuationRing : ∀ {k : Type u_2} [inst : Field k], IsDiscreteValuationRing (PowerSeries k)
-- Mathlib.Algebra.Group.Hom.Defs
instInhabitedMulHom : {M : Type u_4} → {N : Type u_5} → [inst : Mul M] → [inst_1 : MulOneClass N] → Inhabited (M →ₙ* N)
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Slice.Pos.nextn.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Algebra.MvPolynomial.Funext
MvPolynomial.constantCoeff.eq_1 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R],
  MvPolynomial.constantCoeff =
    { toFun := MvPolynomial.coeff 0, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxcIterator.step.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β)
  (it : Std.DTreeMap.Internal.Zipper α β) (upper : α),
  { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper }.step =
    if (compare k upper).isLE = true then
      Std.IterStep.yield { internalState := { iter := Std.DTreeMap.Internal.Zipper.prependMap t it, upper := upper } }
        ⟨k, v⟩
    else Std.IterStep.done
-- Mathlib.Logic.Relator
Relator.BiTotal.rel_exists : ∀ {α : Sort u₁} {β : Sort u₂} {R : α → β → Prop},
  Relator.BiTotal R → Relator.LiftFun (Relator.LiftFun R Iff) Iff (fun p => ∃ i, p i) fun q => ∃ i, q i
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ofList_eq_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {l : List (α × β)},
  Std.ExtDTreeMap.Const.ofList l cmp = List.foldl (fun acc p => acc.insert p.1 p.2) ∅ l
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsAlt.eq_iff : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁]
  {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.IsAlt → ∀ {x y : M₁}, (B x) y = 0 ↔ (B y) x = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldlM_eq_foldlM_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ},
  Std.TreeMap.foldlM f init t = Array.foldlM (fun a b => f a b.1 b.2) init t.toArray
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.mk.inj : ∀ {toTopCat : TopCat} {is_alexandrovDiscrete : AlexandrovDiscrete ↑toTopCat} {toTopCat_1 : TopCat}
  {is_alexandrovDiscrete_1 : AlexandrovDiscrete ↑toTopCat_1},
  { toTopCat := toTopCat, is_alexandrovDiscrete := is_alexandrovDiscrete } =
      { toTopCat := toTopCat_1, is_alexandrovDiscrete := is_alexandrovDiscrete_1 } →
    toTopCat = toTopCat_1
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.lintegral_parallelComp_symm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel γ δ} [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η]
  (ac : α × γ) {g : β × δ → ENNReal},
  Measurable g → ∫⁻ (bd : β × δ), g bd ∂(κ.parallelComp η) ac = ∫⁻ (d : δ), ∫⁻ (b : β), g (b, d) ∂κ ac.1 ∂η ac.2
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- **Alias** of `Set.neg_ofPred`. -/
Set.neg_setOf : ∀ {α : Type u_2} [inst : Neg α] (p : α → Prop), -{x | p x} = {x | p (-x)}
-- Std.Http.Protocol.H1
/-- Validates an incoming request head and selects the body framing mode.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.checkReceivingMessageHead : Std.Http.Protocol.H1.Message.Head Std.Http.Protocol.H1.Direction.receiving →
  Except Std.Http.Protocol.H1.Error Std.Http.Protocol.H1.Machine.BodyMode✝
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∈ m₂ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `F.cocones` is corepresentable, then the cocone corresponding to the identity morphism on
the representing object is a colimit cocone.
 -/
CategoryTheory.Limits.IsColimit.ofCorepresentableBy : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {X : C} →
            (h : F.cocones.CorepresentableBy X) →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.IsColimit.OfNatIso.colimitCocone h)
-- Mathlib.CategoryTheory.Countable
/-- The constructed category is indeed equivalent to `α`.  -/
CategoryTheory.CountableCategory.homAsTypeEquiv : (α : Type u) →
  [inst : CategoryTheory.Category.{v, u} α] →
    [inst_1 : CategoryTheory.CountableCategory α] → CategoryTheory.CountableCategory.HomAsType α ≌ α
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.toList_nil : ∀ {α : Type u_1}, FreeAddMonoid.toList [] = []
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.lift_conj_eq_mul_mul_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X G : C}
  [inst_2 : CategoryTheory.GrpObj G] (f₁ f₂ : X ⟶ G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂)
      (CategoryTheory.GrpObj.conj G) =
    f₁ * f₂ * f₁⁻¹
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.centralizer_univ : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A],
  NonUnitalSubalgebra.centralizer R Set.univ = NonUnitalSubalgebra.center R A
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.mk.inj : ∀ {carrier : Type u} {str : Mul carrier} {carrier_1 : Type u} {str_1 : Mul carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsMinor.exists_eq_contract_delete_disjoint : ∀ {α : Type u_1} {M N : Matroid α}, N ≤m M → ∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = (M.contract C).delete D
-- Mathlib.GroupTheory.Finiteness
Group.fg_of_finite : ∀ {G : Type u_3} [inst : Group G] [Finite G], Group.FG G
-- Init.Data.SInt.Lemmas
Int32.add_right_neg : ∀ (a : Int32), a + -a = 0
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.mk.inj : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language}
  {onFunction : autoParam (⦃n : ℕ⦄ → L.Functions n → L'.Functions n) FirstOrder.Language.LHom.onFunction._autoParam}
  {onRelation : autoParam (⦃n : ℕ⦄ → L.Relations n → L'.Relations n) FirstOrder.Language.LHom.onRelation._autoParam}
  {onFunction_1 : autoParam (⦃n : ℕ⦄ → L.Functions n → L'.Functions n) FirstOrder.Language.LHom.onFunction._autoParam}
  {onRelation_1 : autoParam (⦃n : ℕ⦄ → L.Relations n → L'.Relations n) FirstOrder.Language.LHom.onRelation._autoParam},
  { onFunction := onFunction, onRelation := onRelation } = { onFunction := onFunction_1, onRelation := onRelation_1 } →
    onFunction = onFunction_1 ∧ onRelation = onRelation_1
-- Init.Grind.Config
/-- If `extAll` is `true`, `grind` uses any extensionality theorems available in the environment.  -/
Lean.Grind.Config.extAll : Lean.Grind.Config → Bool
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure.0.Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.match_3.eq_2 : ∀ (motive : Std.Tactic.BVDecide.Gate → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.Gate.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.Gate.xor) (h_3 : Unit → motive Std.Tactic.BVDecide.Gate.beq)
  (h_4 : Unit → motive Std.Tactic.BVDecide.Gate.or),
  (match Std.Tactic.BVDecide.Gate.xor with
    | Std.Tactic.BVDecide.Gate.and => h_1 ()
    | Std.Tactic.BVDecide.Gate.xor => h_2 ()
    | Std.Tactic.BVDecide.Gate.beq => h_3 ()
    | Std.Tactic.BVDecide.Gate.or => h_4 ()) =
    h_2 ()
-- Batteries.Data.AssocList
Batteries.AssocList.forIn.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {δ : Type u_1} [inst : Monad m] (as : Batteries.AssocList α β)
  (init : δ) (f : α × β → δ → m (ForInStep δ)),
  as.forIn init f =
    match as with
    | Batteries.AssocList.nil => pure init
    | Batteries.AssocList.cons k v es => do
      let __do_lift ← f (k, v) init
      match __do_lift with
        | ForInStep.done d => pure d
        | ForInStep.yield d => es.forIn d f
-- Std.Do.PredTrans
Std.Do.PredTrans.ext : ∀ {ps : Std.Do.PostShape} {α : Type u} {t₁ t₂ : Std.Do.PredTrans ps α},
  (∀ (Q : Std.Do.PostCond α ps), t₁.apply Q = t₂.apply Q) → t₁ = t₂
-- Aesop.Util.UnorderedArraySet
Aesop.UnorderedArraySet.ofHashSet : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashSet α → Aesop.UnorderedArraySet α
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
Rep.norm_comp_d_eq_zero_apply : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] (M : Rep.{max u u_1, u, u} R G) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.d₀₁ M)) (M.ρ.norm x) = 0
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof : Type
-- Mathlib.Topology.Connected.Basic
ContinuousOn.mapsTo_connectedComponentIn : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s → ∀ {a : α}, a ∈ s → Set.MapsTo f (connectedComponentIn s a) (connectedComponentIn (f '' s) (f a))
-- Mathlib.Order.Hom.Lattice
/-- Reinterpret a supremum homomorphism as an infimum homomorphism between the dual lattices.  -/
SupHom.dual : {α : Type u_2} → {β : Type u_3} → [inst : Max α] → [inst_1 : Max β] → SupHom α β ≃ InfHom αᵒᵈ βᵒᵈ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.one_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.GrpObj G],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.GrpObj.inv = CategoryTheory.MonObj.one
-- Init.Data.String.Decode
UInt8.utf8ByteSize_pos : ∀ (c : UInt8) (h : c.IsUTF8FirstByte), 0 < c.utf8ByteSize h
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.ιHeart_obj_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {H : Type u'} [inst_6 : CategoryTheory.Category.{v', u'} H]
  [inst_7 : CategoryTheory.Preadditive H] [inst_8 : t.Heart H] (X : H), t.heart (t.ιHeart.obj X)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- The walk obtained by removing the first `n` darts of a walk.  -/
SimpleGraph.Walk.drop : {V : Type u} → {G : SimpleGraph V} → {u v : V} → (p : G.Walk u v) → (n : ℕ) → G.Walk (p.getVert n) v
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.algebraMap_cartanMatrixIn_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Type u_5) [inst_5 : CommRing S]
  [inst_6 : Algebra S R] {P : RootPairing ι R M N} [inst_7 : P.IsValuedIn S] (b : P.Base) (i j : ↥b.support),
  (algebraMap S R) (RootPairing.Base.cartanMatrixIn S b i j) = P.pairing ↑i ↑j
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_comap_eq_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f → ∀ (S : Submonoid N), Submonoid.map f (Submonoid.comap f S) = S
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.completeSemilatticeInf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      [CategoryTheory.WellPowered.{w, v₁, u₁} C] →
        [CategoryTheory.Limits.HasWidePullbacks C] → {B : C} → CompleteSemilatticeInf (CategoryTheory.Subobject B)
-- Init.Tactics
/-- Like `intro`, but introducing stateful hypotheses into the stateful context of the `Std.Do.SPred`
proof mode.
That is, given a stateful goal `(hᵢ : Hᵢ)* ⊢ₛ P → T`, `mintro h` transforms
into `(hᵢ : Hᵢ)*, (h : P) ⊢ₛ T`.

Furthermore, `mintro ∀s` is like `intro s`, but preserves the stateful goal.
That is, `mintro ∀s` brings the topmost state variable `s:σ` in scope and transforms
`(hᵢ : Hᵢ)* ⊢ₛ T` (where the entailment is in `Std.Do.SPred (σ::σs)`) into
`(hᵢ : Hᵢ s)* ⊢ₛ T s` (where the entailment is in `Std.Do.SPred σs`).

Beyond that, `mintro` supports the full syntax of `mcases` patterns
(`mintro pat = (mintro h; mcases h with pat`), and can perform multiple
introductions in sequence.
 -/
Lean.Parser.Tactic.mintroMacro : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
Matrix.instDecidableIsPivotedByOfFintype : {m : Type u_1} →
  {n : Type u_2} →
    {R : Type u_3} →
      [inst : Zero R] →
        [DecidableEq R] →
          [Fintype m] →
            [inst_3 : LinearOrder m] →
              [Fintype n] →
                [inst_5 : LinearOrder n] → (A : Matrix m n R) → (l : m → WithTop n) → Decidable (A.IsPivotedBy l)
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_eq_limsup : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop},
  Filter.blimsup u f p = Filter.limsup u (f ⊓ Filter.principal {x | p x})
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x)
  [inst_2 : CategoryTheory.Bicategory.Lan.CommuteWith f g h],
  (CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso f g h).hom =
    CategoryTheory.Bicategory.lanDesc ((CategoryTheory.Bicategory.lanLeftExtension f g).whisker h)
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∉ m₂ → (m₁ ∪ m₂).get! k = m₁.get! k
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] [inst_1 : SizeOf C] (J : Type v) (U : J → C) (V : J × J → C)
  (f : (i j : J) → V (i, j) ⟶ U i)
  (f_mono : autoParam (∀ (i j : J), CategoryTheory.Mono (f i j)) CategoryTheory.GlueData.f_mono._autoParam)
  (f_hasPullback :
    autoParam (∀ (i j k : J), CategoryTheory.Limits.HasPullback (f i j) (f i k))
      CategoryTheory.GlueData.f_hasPullback._autoParam)
  (f_id : autoParam (∀ (i : J), CategoryTheory.IsIso (f i i)) CategoryTheory.GlueData.f_id._autoParam)
  (t : (i j : J) → V (i, j) ⟶ V (j, i)) (t_id : ∀ (i : J), t i i = CategoryTheory.CategoryStruct.id (V (i, i)))
  (t' : (i j k : J) → CategoryTheory.Limits.pullback (f i j) (f i k) ⟶ CategoryTheory.Limits.pullback (f j k) (f j i))
  (t_fac :
    ∀ (i j k : J),
      CategoryTheory.CategoryStruct.comp (t' i j k) (CategoryTheory.Limits.pullback.snd (f j k) (f j i)) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (f i j) (f i k)) (t i j))
  (cocycle :
    ∀ (i j k : J),
      CategoryTheory.CategoryStruct.comp (t' i j k) (CategoryTheory.CategoryStruct.comp (t' j k i) (t' k i j)) =
        CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (f i j) (f i k))),
  sizeOf
      { J := J, U := U, V := V, f := f, f_mono := f_mono, f_hasPullback := f_hasPullback, f_id := f_id, t := t,
        t_id := t_id, t' := t', t_fac := t_fac, cocycle := cocycle } =
    1 + sizeOf J
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.comp_injective : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : CommGroup α] [IsUniformGroup α]
  {f : β → α} [CompleteSpace α] {i : γ → β}, Multipliable f → Function.Injective i → Multipliable (f ∘ i)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_eval_neg : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ) (x : R),
  Polynomial.eval (-x) (Polynomial.Chebyshev.T R n) = ↑↑n.negOnePow * Polynomial.eval x (Polynomial.Chebyshev.T R n)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C), ((t.triangleLTGE n).obj j).obj₁ = (t.truncLT n).obj j
-- Mathlib.Data.Finsupp.Order
Finsupp.isOrderedCancelAddMonoid : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelAddMonoid α],
  IsOrderedCancelAddMonoid (ι →₀ α)
-- Mathlib.Algebra.Category.AlgCat.FilteredColimits
instCreatesColimitsOfShapeAlgCatRingCatForget₂AlgHomCarrierRingHomCarrierOfIsFiltered : {R : Type u} →
  [inst : CommRing R] →
    {J : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
        [CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget RingCat)] →
          [CategoryTheory.IsFiltered J] →
            CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.forget₂ (AlgCat R) RingCat)
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingCoeff_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.trailingCoeff = 0 ↔ p = 0
-- Mathlib.Data.ZMod.Basic
ZMod.val_add_of_le : ∀ {n : ℕ} [NeZero n] {a b : ZMod n}, n ≤ a.val + b.val → (a + b).val = a.val + b.val - n
-- Mathlib.Lean.Name
/-- Retrieve all names in the environment satisfying a predicate.
 -/
allNames : (Lean.Name → Bool) → Lean.CoreM (Array Lean.Name)
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instSub.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Sub (G i)], Pi.instSub = { sub := fun f g i => f i - g i }
-- Mathlib.RingTheory.Flat.Equalizer
_private.Mathlib.RingTheory.Flat.Equalizer.0.LinearMap.lTensor_eqLocus_subtype_tensorEqLocusInv : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f g : N →ₗ[R] P) [inst_11 : Module.Flat R M]
  (x :
    ↥(((TensorProduct.AlgebraTensorModule.lTensor S M) f).eqLocus ((TensorProduct.AlgebraTensorModule.lTensor S M) g))),
  (LinearMap.lTensor M (f.eqLocus g).subtype) ((LinearMap.tensorEqLocusInv S M f g) x) = ↑x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List α} {k k' : α},
      cmp k k' = Ordering.eq →
        ∀ {h' : k' ∈ Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l},
          k ∉ t →
            List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
              k ∈ l → (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).getKey k' h' = k
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.mk.sizeOf_spec : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : SizeOf R]
  [inst_4 : SizeOf S] (P : StandardEtalePair R) (x : S) (hasMap : P.HasMap x)
  (lift_bijective : Function.Bijective ⇑(P.lift x hasMap)),
  sizeOf { P := P, x := x, hasMap := hasMap, lift_bijective := lift_bijective } =
    1 + sizeOf P + sizeOf x + sizeOf hasMap + sizeOf lift_bijective