mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.fold_filterM : ∀ {α β δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Monad n] [inst_3 : MonadAttach n] [WeaklyLawfulMonadAttach n] [inst_5 : Std.Internal.Do.Assertion Pred]
  [inst_6 : Std.Internal.Do.Assertion EPred] [inst_7 : Std.Internal.Do.WPMonad n Pred EPred]
  [inst_8 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → n (ULift.{w, 0} Bool)} {g : δ → β → δ}
  {init : δ} {it : Std.Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.Iter.foldM
        (fun d b => do
          let __do_lift ← f b
          pure (if __do_lift.down = true then g d b else d))
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.Iter.filterM f it) ⦃ Q; eQ ⦄
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.adjunction_counit_map_functor : ∀ {X : TopCat} {U : TopologicalSpace.Opens ↑X} (V : TopologicalSpace.Opens ↥U),
  ⋯.adjunction.counit.app (⋯.functor.obj V) = CategoryTheory.eqToHom ⋯
-- Init.Grind.Attr
/-- Like `@[grind]`, but enforces the **minimal indexable subexpression condition**:
when several subterms cover the same free variables, `grind!` chooses the smallest one.

This influences E-matching pattern selection.

### Example
```lean
theorem fg_eq (h : x > 0) : f (g x) = x

@[grind <-] theorem fg_eq (h : x > 0) : f (g x) = x
-- Pattern selected: `f (g x)`

-- With minimal subexpression:
@[grind! <-] theorem fg_eq (h : x > 0) : f (g x) = x
-- Pattern selected: `g x`
```
 -/
Lean.Parser.Attr.grind! : Lean.ParserDescr
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.single_injective : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → Zero (M i)] [inst_1 : DecidableEq ι] (i : ι),
  Function.Injective (Pi.single i)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp],
  t.WF → t.isEmpty = false → ∀ {km fallback : α}, t.maxKeyD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Init.Data.RArray
_private.Init.Data.RArray.0.Lean.RArray.get_eq_def.match_1.splitter : {α : Type u_1} →
  (motive : Lean.RArray α → Sort u_2) →
    (a : Lean.RArray α) →
      ((x : α) → motive (Lean.RArray.leaf x)) →
        ((p : ℕ) → (l r : Lean.RArray α) → motive (Lean.RArray.branch p l r)) → motive a
-- Mathlib.MeasureTheory.Function.Jacobian
/-- Change of variable formula for differentiable functions, set version: if a function `f` is
injective and differentiable on a measurable set `s`, then the pushforward of the measure with
density `|(f' x).det|` on `s` is the Lebesgue measure on the image set. This version is expressed
in terms of the restricted function `s.domRestrict f`.
For a version for the original function, see `map_withDensity_abs_det_fderiv_eq_addHaar`.
 -/
MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasurableSet s →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
      Set.InjOn f s →
        MeasureTheory.Measure.map (s.domRestrict f)
            (MeasureTheory.Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) =
          μ.restrict (f '' s)
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate : Type
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct Z] (b : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct Z).inv
      (CategoryTheory.Limits.Sigma.ι Z b).op =
    CategoryTheory.Limits.Pi.π (fun x => Opposite.op (Z x)) b
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight_cons_cons_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {n : ℕ} (a : K) (x : Fin n → K),
  Height.logHeight (Matrix.vecCons a (Matrix.vecCons 0 x)) = Height.logHeight (Matrix.vecCons a x)
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.coe_bot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LE α], ↑⊥ = ∅
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
HasCardinalLT.small : ∀ {X : Type u} {κ : Cardinal.{v}}, HasCardinalLT X κ → Small.{v, u} X
-- Mathlib.Topology.EMetricSpace.Defs
/-- A pseudo extended metric space is a type endowed with a `ℝ≥0∞`-valued distance `edist`
satisfying reflexivity `edist x x = 0`, commutativity `edist x y = edist y x`, and the triangle
inequality `edist x z ≤ edist x y + edist y z`.

Note that we do not require `edist x y = 0 → x = y`. See extended metric spaces (`EMetricSpace`) for
the similar class with that stronger assumption.

Any pseudo extended metric space is a topological space and a uniform space (see `TopologicalSpace`,
`UniformSpace`), where the topology and uniformity come from the metric.
Note that a T1 pseudo extended metric space is just an extended metric space.

We make the uniformity/topology part of the data instead of deriving it from the metric. This e.g.
ensures that we do not get a diamond when doing
`[PseudoEMetricSpace α] [PseudoEMetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance].  -/
PseudoEMetricSpace : Type u → Type u
-- Mathlib.Data.Int.Bitwise
Int.bitwise_and : Int.bitwise and = Int.land
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.left_le_opow : ∀ (a : Ordinal.{u_1}) {b : Ordinal.{u_1}}, 0 < b → a ≤ a ^ b
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.homologySequenceδ_triangleh : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁),
  (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).homologySequenceδ
      (CochainComplex.mappingCone.triangleh S.f) n₀ n₁ h =
    CategoryTheory.CategoryStruct.comp
      ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₀).hom.app (CochainComplex.mappingCone S.f))
      (CategoryTheory.CategoryStruct.comp
        (HomologicalComplex.homologyMap (CochainComplex.mappingCone.descShortComplex S) n₀)
        (CategoryTheory.CategoryStruct.comp (hS.δ n₀ n₁ h)
          ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₁).inv.app S.X₁)))
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
/-- `Equiv.mulRight₀` as an order isomorphism.  -/
OrderIso.mulRight₀ : {G₀ : Type u_1} →
  [inst : GroupWithZero G₀] → [inst_1 : PartialOrder G₀] → [MulPosReflectLT G₀] → (a : G₀) → 0 < a → G₀ ≃o G₀
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.piBinderTypes : Lean.Option Bool
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ \ m₂).getKey? k = none
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Submonoid.LocalizationMap.map_zero : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  (f : S.LocalizationMap N), f 0 = 0
-- Init.Core
Subtype.eta : ∀ {α : Sort u} {p : α → Prop} (a : { x // p x }) (h : p ↑a), ⟨↑a, h⟩ = a
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.ofπ_π : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (π : (relations.G →₀ A) →ₗ[A] M) (hπ : ∀ (r : relations.R), π (relations.relation r) = 0),
  (Module.Relations.Solution.ofπ π hπ).π = π
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanSingleton_le_iff_mem : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] {x : P} {I : FractionalIdeal S P}, FractionalIdeal.spanSingleton S x ≤ I ↔ x ∈ I
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_lt_intCast : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {m : ℚ} {n : ℤ}, ↑m < ↑n ↔ m < ↑n
-- Mathlib.CategoryTheory.Limits.Types.Images
/-- the factorisation of any morphism in Type through a mono.  -/
CategoryTheory.Limits.Types.monoFactorisation : {α β : Type u} → (f : α ⟶ β) → CategoryTheory.Limits.MonoFactorisation f
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_eq_zero : ∀ {x : ENNReal}, ↑x = 0 ↔ x = 0
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.apply_mk_symm : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : ∀ (x : B), Nonempty (E x)] (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) {b : B},
  b ∈ e.baseSet → ∀ (y : F), ↑e ⟨b, e.symm b y⟩ = (b, y)
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_ofNatClamp_of_lt : ∀ {n : ℕ}, n < UInt64.size → (UInt64.ofNatClamp n).toUInt8 = UInt8.ofNat n
-- Mathlib.Data.Finset.Union
Finset.disjiUnion_filter_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (s : Finset α) (t : Finset β) (f : α → β),
  t.disjiUnion (fun a => {x ∈ s | f x = a}) ⋯ = {c ∈ s | f c ∈ t}
-- Mathlib.Data.ZMod.Basic
ZMod.nontrivial : ∀ (n : ℕ) [Fact (1 < n)], Nontrivial (ZMod n)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryLT!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α}, t₁.Equiv t₂ → t₁.getEntryLT! k = t₂.getEntryLT! k
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelComparison_comp_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)] {Z : D} (h : G.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelComparison f G)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (G.map f)) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.kernel.ι f)) h
-- Mathlib.Order.WithBot
WithTop.map₂_coe_coe : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β), WithTop.map₂ f ↑a ↑b = ↑(f a b)
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.State.congrInfo : Lean.Meta.Sym.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.CongrInfo
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiff_infty : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  ContDiff 𝕜 (↑⊤) f ↔ ∀ (n : ℕ), ContDiff 𝕜 (↑n) f
-- Init.GrindInstances.ToInt
Lean.Grind.instModFinCoOfNatIntCast : ∀ {n : ℕ}, Lean.Grind.ToInt.Mod (Fin n) (Lean.Grind.IntInterval.co 0 ↑n)
-- Mathlib.Order.Bounded
Set.unbounded_lt_iff_unbounded_le : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α] [NoMaxOrder α],
  Set.Unbounded (fun x1 x2 => x1 < x2) s ↔ Set.Unbounded (fun x1 x2 => x1 ≤ x2) s
-- Mathlib.Tactic.ITauto
/-- A decision procedure for intuitionistic propositional logic.

* `useDec` will add `a ∨ ¬ a` to the context for every decidable atomic proposition `a`.
* `useClassical` will allow `a ∨ ¬ a` to be added even if the proposition is not decidable,
  using classical logic.
* `extraDec` will add `a ∨ ¬ a` to the context for specified (not necessarily atomic)
  propositions `a`.
 -/
Mathlib.Tactic.ITauto.itautoCore : Lean.MVarId → Bool → Bool → Array Lean.Expr → Lean.MetaM Unit
-- Mathlib.Analysis.Complex.Polynomial.Basic
Polynomial.mul_star_dvd_of_aeval_eq_zero_im_ne_zero : ∀ (p : Polynomial ℝ) {z : ℂ},
  (Polynomial.aeval z) p = 0 →
    z.im ≠ 0 →
      (Polynomial.X - Polynomial.C ((starRingEnd ℂ) z)) * (Polynomial.X - Polynomial.C z) ∣
        Polynomial.map (algebraMap ℝ ℂ) p
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocCommSemiring.mk : {α : Type u} →
  [toNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring α] →
    (∀ (a b : α), a * b = b * a) → NonUnitalNonAssocCommSemiring α
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.norm_def : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂), ‖f‖ = sInf {c | 0 ≤ c ∧ ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass.0.tacticMap_simp : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normal_iff_map_addConj_eq : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  H.Normal ↔ ∀ (g : G), AddSubgroup.map (↑(AddAut.addConj g)) H = H
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.IsLocalizingSequence.toIsPreLocalizingSequence : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : Preorder ι] [inst_1 : TopologicalSpace ι]
  [inst_2 : OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : ℕ → Ω → WithTop ι}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsLocalizingSequence._auto_1},
  ProbabilityTheory.IsLocalizingSequence 𝓕 τ P → ProbabilityTheory.IsPreLocalizingSequence 𝓕 τ P
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.LinearEquiv.coe_lift_symm : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (g : M ≃ₗ[R] N),
  ↑(DividedPowerAlgebra.mapEquiv g).symm = DividedPowerAlgebra.map R ↑g.symm
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHint : Type
-- Mathlib.Algebra.Group.Basic
neg_add_eq_neg_add_iff_add_eq_add : ∀ {G : Type u_3} [inst : AddCommGroup G] {a b c d : G}, -b + a = -d + c ↔ a + d = c + b
-- Mathlib.Analysis.Convex.Basic
Set.Subsingleton.convex : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, s.Subsingleton → Convex 𝕜 s
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.tendsto_measure_iUnion_atBot : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Preorder ι]
  [Filter.atBot.IsCountablyGenerated] {s : ι → Set α},
  Antitone s → Filter.Tendsto (⇑μ ∘ s) Filter.atBot (nhds (μ (⋃ n, s n)))
-- Mathlib.Computability.NFA
NFA.pumping_lemma : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} [inst : Fintype σ] {x : List α},
  x ∈ M.accepts →
    Fintype.card (Set σ) ≤ x.length →
      ∃ a b c,
        x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * KStar.kstar {b} * {c} ≤ M.accepts
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.le_def : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : PartialOrder β]
  {f g : C(α, β)}, f ≤ g ↔ ∀ (a : α), f a ≤ g a
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBySet_annihilator_top : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.IsTorsionBySet R M ↑⊤.annihilator
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.intCast : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n] [NoZeroDivisors R] (d : ℤ), 0 < d → (↑d).PosDef
-- Mathlib.RingTheory.Finiteness.Basic
/-- The sup of two fg submodules is finite. Also see `Submodule.FG.sup`.  -/
Submodule.finite_sup : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] (S₁ S₂ : Submodule R V)
  [h₁ : Module.Finite R ↥S₁] [h₂ : Module.Finite R ↥S₂], Module.Finite R ↥(S₁ ⊔ S₂)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.mk_inv : ∀ {M : Type u_1} [inst : Inv M] (a : M), DomMulAct.mk a⁻¹ = (DomMulAct.mk a)⁻¹
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {x y : α},
  x ≠ 0 →
    y ≠ 0 →
      UniqueFactorizationMonoid.normalizedFactors (x * y) =
        UniqueFactorizationMonoid.normalizedFactors x + UniqueFactorizationMonoid.normalizedFactors y
-- Mathlib.Algebra.Module.Presentation.Free
/-- If `relations : Relations A` involves no relations (`[IsEmpty relations.R]`),
then the free module `relations.G →₀ A` satisfies the universal property of the
corresponding module defined by generators (and relations).  -/
Module.Relations.solutionFinsupp.isPresentationCore : {A : Type u} →
  [inst : Ring A] →
    (relations : Module.Relations A) → [inst_1 : IsEmpty relations.R] → relations.solutionFinsupp.IsPresentationCore
-- Init.Data.Array.Count
Array.size_eq_countP_add_countP : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α},
  xs.size = Array.countP p xs + Array.countP (fun a => decide ¬p a = true) xs
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_eq_empty : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, -s = ∅ ↔ s = ∅
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftHom.leftUnitorHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : C) →
        [inst_2 : Mathlib.Tactic.Coherence.LiftObj X] →
          Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
-- Mathlib.Tactic.NormNum.Pow
/-- This is an opaque wrapper around `Nat.pow` to prevent lean from unfolding the definition of
`Nat.pow` on numerals. The arbitrary precondition `p` is actually a formula of the form
`Nat.pow a' b' = c'` but we usually don't care to unfold this proposition so we just carry a
reference to it.  -/
Mathlib.Meta.NormNum.IsNatPowT : Prop → ℕ → ℕ → ℕ → Prop
-- Init.Tactics
/-- A `generalize` argument, of the form `term = x` or `h : term = x`.  -/
Lean.Parser.Tactic.generalizeArg : Lean.ParserDescr
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.subtypeCongr.right_apply_subtype : ∀ {ε : Type u_9} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a })
  (a : { a // ¬p a }), (ep.subtypeCongr en) ↑a = ↑(en a)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.isLE_truncLE_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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) (X : C) (a b : ℤ),
  autoParam (a ≤ b) CategoryTheory.Triangulated.TStructure.isLE_truncLE_obj._auto_1 → t.IsLE ((t.truncLE a).obj X) b
-- Mathlib.Algebra.Homology.QuasiIso
quasiIsoAt_iff_exactAt' : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i], L.ExactAt i → (QuasiIsoAt f i ↔ K.ExactAt i)
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.defEvalConfigItem.mkTrie : Lean.Syntax →
  Lean.Ident →
    Lean.Elab.ConfigEval.EvalConfigItemView →
      Lean.Name → Bool → Lean.Elab.ConfigEval.M✝ Lean.Elab.ConfigEval.HandlerTrie✝
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.instInvertibleNatToArithmeticFunctionZeta : {R : Type u_1} → [inst : CommRing R] → Invertible ↑ArithmeticFunction.zeta
-- Init.Data.ToString.Basic
instToStringDecidable : {p : Prop} → ToString (Decidable p)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft' : ∀ {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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x y : C} (f : x ⟶ y)
  [inst_4 : CategoryTheory.IsIso f] (z : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft (CategoryTheory.inv f) z)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f z) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj y z)
-- Mathlib.Topology.Order
instDiscreteTopologyInt : DiscreteTopology ℤ
-- Init.Data.Range.Polymorphic.SInt
Int64.instRxiHasSize : Std.Rxi.HasSize Int64
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k k' : α},
  m.getKey? k = some k' → (Std.ExtHashMap.map f m)[k]? = Option.map (f k') m[k]?
-- Lean.Attributes
Lean.ParametricAttributeImpl.getParam : {α : Type} → Lean.ParametricAttributeImpl α → Lean.Name → Lean.Syntax → Lean.AttrM α
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- A variant of `appIso_hom` that uses `Hom.appLE`.  -/
AlgebraicGeometry.Scheme.Hom.appIso_hom' : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens),
  (AlgebraicGeometry.Scheme.Hom.appIso f U).hom =
    AlgebraicGeometry.Scheme.Hom.appLE f ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U) U ⋯
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.toAddMonoidHom_eq_coe : ∀ {α : Type u_2} {β : Type u_3} {x : Preorder α} {x_1 : Preorder β} {x_2 : AddZeroClass α} {x_3 : AddZeroClass β}
  (f : α →+o β), f.toAddMonoidHom = ↑f
-- Mathlib.Algebra.Module.Equiv.Basic
/-- If `M` and `M₂` are linearly isomorphic then the endomorphism rings of `M` and `M₂`
are isomorphic.

See `LinearEquiv.conj` for the linear version of this isomorphism.  -/
LinearEquiv.conjRingEquiv : {R₁ : Type u_9} →
  {R₂ : Type u_10} →
    {M₁ : Type u_13} →
      {M₂ : Type u_14} →
        [inst : Semiring R₁] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M₁] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R₁ M₁] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R₁ →+* R₂} →
                      {σ₂₁ : R₂ →+* R₁} →
                        [inst_6 : RingHomInvPair σ₁₂ σ₂₁] →
                          [inst_7 : RingHomInvPair σ₂₁ σ₁₂] → (M₁ ≃ₛₗ[σ₁₂] M₂) → Module.End R₁ M₁ ≃+* Module.End R₂ M₂
-- Std.Data.HashMap.Lemmas
Std.HashMap.not_mem_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a : α}, a ∉ ∅
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_insertMany_empty_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : Std.LawfulEqOrd α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k},
  List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).get? k' = some (cast ⋯ v)
-- Mathlib.Data.Multiset.Fintype
/-- `v ::ₘ m` is equivalent to `Option m` by mapping one `v` to `none` and everything else to `m`.
 -/
Multiset.consEquiv : {α : Type u_1} → [inst : DecidableEq α] → {m : Multiset α} → {v : α} → (v ::ₘ m).ToType ≃ Option m.ToType
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.eq_zero_of_eq_zero : ∀ {R : Type u_1} [inst : Semiring R], 0 = 1 → ∀ (p : SkewPolynomial R), p = 0
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.card_pair_lcm_eq : ∀ {n : ℕ},
  Squarefree n → {p ∈ n.divisors ×ˢ n.divisors | p.1.lcm p.2 = n}.card = 3 ^ ArithmeticFunction.cardDistinctFactors n