mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
CategoryTheory.MorphismProperty.instIsStableUnderFilteredColimitsMonomorphismsOfAB5OfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasFilteredColimitsOfSize.{v', u', v, u} C]
  [CategoryTheory.AB5OfSize.{v', u', v, u} C],
  CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits.{v', u', v, u}
    (CategoryTheory.MorphismProperty.monomorphisms C)
-- Mathlib.Analysis.InnerProductSpace.Spectrum
_private.Mathlib.Analysis.InnerProductSpace.Spectrum.0.LinearMap.IsSymmetric.unsortedEigenvectorBasis.congr_simp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T T_1 : E →ₗ[𝕜] E} (e_T : T = T_1) [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric)
  (hn : Module.finrank 𝕜 E = n),
  LinearMap.IsSymmetric.unsortedEigenvectorBasis✝ hT hn = LinearMap.IsSymmetric.unsortedEigenvectorBasis✝ ⋯ hn
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.invtRootSubmodule.bot_mem : ∀ {ι : 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] (P : RootPairing ι R M N),
  ⊥ ∈ P.invtRootSubmodule
-- Lean.Util.PPExt
Lean.PPFns.mk.inj : ∀ {ppExprWithInfos : Lean.PPContext → Lean.Expr → IO Lean.FormatWithInfos}
  {ppConstNameWithInfos : Lean.PPContext → Lean.Name → IO Lean.FormatWithInfos}
  {ppTerm : Lean.PPContext → Lean.Term → IO Std.Format} {ppLevel : Lean.PPContext → Lean.Level → IO Std.Format}
  {ppGoal : Lean.PPContext → Lean.MVarId → IO Std.Format}
  {ppExprWithInfos_1 : Lean.PPContext → Lean.Expr → IO Lean.FormatWithInfos}
  {ppConstNameWithInfos_1 : Lean.PPContext → Lean.Name → IO Lean.FormatWithInfos}
  {ppTerm_1 : Lean.PPContext → Lean.Term → IO Std.Format} {ppLevel_1 : Lean.PPContext → Lean.Level → IO Std.Format}
  {ppGoal_1 : Lean.PPContext → Lean.MVarId → IO Std.Format},
  { ppExprWithInfos := ppExprWithInfos, ppConstNameWithInfos := ppConstNameWithInfos, ppTerm := ppTerm,
        ppLevel := ppLevel, ppGoal := ppGoal } =
      { ppExprWithInfos := ppExprWithInfos_1, ppConstNameWithInfos := ppConstNameWithInfos_1, ppTerm := ppTerm_1,
        ppLevel := ppLevel_1, ppGoal := ppGoal_1 } →
    ppExprWithInfos = ppExprWithInfos_1 ∧
      ppConstNameWithInfos = ppConstNameWithInfos_1 ∧ ppTerm = ppTerm_1 ∧ ppLevel = ppLevel_1 ∧ ppGoal = ppGoal_1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_ric_eq_toList_rco : ∀ {n : ℕ}, (*...=n).toList = (0...n + 1).toList
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.map_bot : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S), Subring.map f ⊥ = ⊥
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.beq'_eq : ∀ (p₁ p₂ : Lean.Grind.CommRing.Poly), (p₁.beq' p₂ = true) = (p₁ = p₂)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inr_inr_pushoutRightPushoutInlIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout f' (CategoryTheory.Limits.pushout.inl f g)] {Z_1 : C}
  (h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp f f') g ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f' (CategoryTheory.Limits.pushout.inl f g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutRightPushoutInlIso f g f').hom h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp f f') g) h
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.map_injective_of_injective : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'},
  Function.Injective ⇑f → ∀ (u v : V), Function.Injective (SimpleGraph.Walk.map f)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoIsPullback_inv_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y}
  {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : CategoryTheory.IsPullback fst snd f g)
  (h' : CategoryTheory.IsPullback fst' snd' f g) {Z_1 : C} (h_1 : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').inv
      (CategoryTheory.CategoryStruct.comp snd h_1) =
    CategoryTheory.CategoryStruct.comp snd' h_1
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidal_associator : ∀ (M : Type u) [inst : Monoid M] (x x_1 x_2 : CategoryTheory.Discrete M),
  CategoryTheory.MonoidalCategoryStruct.associator x x_1 x_2 = CategoryTheory.Discrete.eqToIso ⋯
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.id_map_iff : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  AEMeasurable X μ →
    (ProbabilityTheory.HasSubgaussianMGF id c (MeasureTheory.Measure.map X μ) ↔
      ProbabilityTheory.HasSubgaussianMGF X c μ)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_eq_getElem?_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.minKey? = t.keysArray[0]?
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.struct : Option Lean.Name → Array Lean.IR.IRType → Lean.IR.IRType
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Limits.IsZero.projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.Limits.IsZero X → CategoryTheory.Projective X
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.noZeroDivisors : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [NoZeroDivisors A]
  [inst_3 : Module R A] (S : NonUnitalSubalgebra R A), NoZeroDivisors ↥S
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
Std.Tactic.BVDecide.Return : Std.Sat.AIG Std.Tactic.BVDecide.BVBit → Type
-- Lean.Data.Iterators.Producers.PersistentHashMap
/-- Counts the total remaining work in a zipper, including entries nested in child nodes.  -/
Lean.PersistentHashMap.Zipper.measure : {α : Type u_1} → {β : Type u_2} → Lean.PersistentHashMap.Zipper α β → ℕ
-- Mathlib.Tactic.NormNum.Result
/-- Assert that an element of a semiring is equal to the coercion of some natural number.  -/
Mathlib.Meta.NormNum.IsNat : {α : Type u} → [AddMonoidWithOne α] → α → ℕ → Prop
-- Plausible.Sampleable
/-- `SampleableExt` can be used in two ways. The first (and most common)
is to simply generate values of a type directly using the `Gen` monad;
if this is what you want to do then declaring an `Arbitrary` instance is the
way to go.

Furthermore it makes it possible to express generators for types that
do not lend themselves to introspection, such as `Nat → Nat`.
If we test a quantification over functions the
counter-examples cannot be shrunken or printed meaningfully.
For that purpose, `SampleableExt` provides a proxy representation
`proxy` that can be printed and shrunken as well
as interpreted (using `interp`) as an object of the right type.  -/
Plausible.SampleableExt : Sort u → Sort (max u (v + 2))
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.RingCompare.mk.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} [inst : (a : Q(«$α»)) → SizeOf (BaseType a)]
  (eq : {x y : Q(«$α»)} → BaseType x → BaseType y → Bool)
  (compare : {x y : Q(«$α»)} → BaseType x → BaseType y → Ordering), sizeOf { eq := eq, compare := compare } = 1
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.coe_toPartialHomeomorph : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), ↑e.toPartialHomeomorph = ↑e
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.box.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (ty : Lean.Expr) (fvarId : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_21),
  sizeOf (Lean.Compiler.LCNF.LetValue.box ty fvarId h) = 1 + sizeOf ty + sizeOf fvarId + sizeOf h
-- Mathlib.Data.Fintype.EquivFin
String.infinite : Infinite String
-- Mathlib.Analysis.Normed.Field.Basic
NormedDivisionRing.mk : {α : Type u_5} →
  [toNorm : Norm α] →
    [toDivisionRing : DivisionRing α] →
      [toMetricSpace : MetricSpace α] →
        (∀ (x y : α), dist x y = ‖-x + y‖) → (∀ (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖) → NormedDivisionRing α
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.toContinuousMap_id : ∀ {R : Type u_3} [inst : Zero R] [inst_1 : TopologicalSpace R] {s : Set R} [inst_2 : Fact (0 ∈ s)],
  ↑(ContinuousMapZero.id s) = ContinuousMap.restrict s (ContinuousMap.id R)
-- Mathlib.Topology.UniformSpace.Equicontinuity
uniformEquicontinuousOn_univ : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] (F : ι → β → α),
  UniformEquicontinuousOn F Set.univ ↔ UniformEquicontinuous F
-- Mathlib.Geometry.Euclidean.Projection
/-- There exists `r` such that `p` has distance `r` from all the
points of a set of points in `s` if and only if there exists (possibly
different) `r` such that its `orthogonalProjection` has that distance
from all the points in that set.  -/
EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {ps : Set P},
  ps ⊆ ↑s →
    ∀ (p : P),
      (∃ r, ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((EuclideanGeometry.orthogonalProjection s) p) = r
-- Mathlib.RingTheory.KrullDimension.Basic
ringKrullDim_nonneg_of_nontrivial : ∀ {R : Type u_1} [inst : CommSemiring R] [Nontrivial R], 0 ≤ ringKrullDim R
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_zero_left : ∀ {R : Type u} [inst : Semiring R] ⦃a : R⦄, (Polynomial.monomial 0) a = Polynomial.C a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.of_toList_perm : ∀ {α : Type u} {β : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β}, t₁.toList.Perm t₂.toList → t₁.Equiv t₂
-- Mathlib.Analysis.Complex.CauchyIntegral
DifferentiableOn.analyticOnNhd : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {s : Set ℂ} {f : ℂ → E},
  DifferentiableOn ℂ f s → IsOpen s → AnalyticOnNhd ℂ f s
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_modify : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : Std.LawfulEqOrd α]
  {t : Std.DTreeMap.Internal.Impl α β} {a : α} {f : β a → β a},
  t.Balanced → t.Ordered → (Std.DTreeMap.Internal.Impl.modify a f t).Ordered
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumLocallyUniformlyOn.summableLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasSumLocallyUniformlyOn f g s → SummableLocallyUniformlyOn f s
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sinh_ofReal_im : ∀ (x : ℝ), (Complex.sinh ↑x).im = 0
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
IsUnramifiedAtInfinitePlaces.bot : ∀ (k : Type u_1) [inst : Field k] (K : Type u_2) [inst_1 : Field K] (F : Type u_3) [inst_2 : Field F]
  [inst_3 : Algebra k K] [inst_4 : Algebra k F] [inst_5 : Algebra K F] [IsScalarTower k K F]
  [h₁ : IsUnramifiedAtInfinitePlaces k F] [Algebra.IsAlgebraic K F], IsUnramifiedAtInfinitePlaces k K
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.Nonempty.some.congr_simp : ∀ {α : Type u} {s s_1 : Set α} (e_s : s = s_1) (h : s.Nonempty), h.some = ⋯.some
-- Lean.Language.Lean.Types
/-- State after successful importing.  -/
Lean.Language.Lean.HeaderProcessedSnapshot.result? : Lean.Language.Lean.HeaderProcessedSnapshot → Option Lean.Language.Lean.HeaderProcessedState
-- Init.Data.Vector.Lemmas
_private.Init.Data.Vector.Basic.0.Vector.mapM.go.congr_simp : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] (f f_1 : α → m β),
  f = f_1 →
    ∀ (xs xs_1 : Vector α n),
      xs = xs_1 →
        ∀ (k : ℕ) (h : k ≤ n) (acc acc_1 : Vector β k),
          acc = acc_1 → Vector.mapM.go✝ f xs k h acc = Vector.mapM.go✝ f_1 xs_1 k h acc_1
-- Init.Data.Array.Basic
/-- Applies the monadic action `f` to each element of an array, in order.

The optional parameters `start` and `stop` control the region of the array to which `f` should be
applied. Iteration proceeds from `start` (inclusive) to `stop` (exclusive), so `f` is not invoked
unless `start < stop`. By default, the entire array is used.
 -/
Array.forM : {α : Type u} →
  {m : Type v → Type w} →
    [Monad m] → (α → m PUnit.{v + 1}) → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → m PUnit.{v + 1}
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (S : CategoryTheory.SplitEpi f.hom) (n : ℕ),
  CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n =
    CategoryTheory.Limits.WidePullback.lift (CategoryTheory.Limits.WidePullback.base fun x => f.hom)
      (fun i =>
        Fin.cases
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => f.hom) S.section_)
          (CategoryTheory.Limits.WidePullback.π fun x => f.hom) i)
      ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.mk_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y),
  (CategoryTheory.Limits.BinaryFan.mk π₁ π₂).snd = π₂
-- Lean.Meta.HaveTelescope
/-- The simplified expression in `(fun x => b) v` form. Note that it may contain loose bound variables.
`simpHaveTelescope` attempts to minimize the quadratic overhead imposed
by the locally nameless discipline in a sequence of `have` expressions.
 -/
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.SimpHaveResult.expr : Lean.Meta.SimpHaveResult✝ → Lean.Expr
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.Hom.ext : ∀ {A B : Semigrp} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Mathlib.Data.Real.Basic
Real.mk_one : Real.mk 1 = 1
-- Mathlib.Algebra.Polynomial.Sequence
Polynomial.Sequence.mk : {R : Type u_1} →
  [inst : Semiring R] → (elems' : ℕ → Polynomial R) → (∀ (i : ℕ), (elems' i).degree = ↑i) → Polynomial.Sequence R
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_comap : ∀ {α : Type ua} {β : Type ub} {f : α → β} [u : UniformSpace β], UniformContinuous f
-- Mathlib.Topology.UniformSpace.DiscreteUniformity
discreteUniformity_iff_eq_principal_setRelId : ∀ {X : Type u_2} [inst : UniformSpace X], DiscreteUniformity X ↔ uniformity X = Filter.principal SetRel.id
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_self_ne_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x : E}, inner 𝕜 x x ≠ 0 ↔ x ≠ 0
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.roleExpandersFor : Lean.Ident →
  Lean.Elab.TermElabM
    (Array
      (Lean.Name ×
        (Lean.TSyntaxArray `inline →
          StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM (Lean.Doc.Inline Lean.ElabInline))))
-- Mathlib.Logic.Equiv.List
Encodable.length_le_encode : ∀ {α : Type u_1} [inst : Encodable α] (l : List α), l.length ≤ Encodable.encode l
-- Mathlib.Data.DFinsupp.Defs
OfNat.ofNat.hcongr_3 : ∀ (α α' : Type u),
  α = α' →
    ∀ (x x' : ℕ), x = x' → ∀ (self : OfNat α x) (self' : OfNat α' x'), self ≍ self' → OfNat.ofNat x ≍ OfNat.ofNat x'
-- Mathlib.Algebra.Field.Periodic
Function.Antiperiodic.mul_const' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : DivisionSemiring α] [inst_1 : Neg β],
  Function.Antiperiodic f c → ∀ {a : α}, a ≠ 0 → Function.Antiperiodic (fun x => f (x * a)) (c / a)
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.mk.inj : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} {inst : Semiring A} {inst_1 : Monoid G} {inst_2 : AddCommMonoid W}
  {inst_3 : Module A W} {ρ : Representation A G W} {toSubmodule : Submodule A W}
  {apply_mem_toSubmodule : ∀ (g : G) ⦃v : W⦄, v ∈ toSubmodule → (ρ g) v ∈ toSubmodule} {toSubmodule_1 : Submodule A W}
  {apply_mem_toSubmodule_1 : ∀ (g : G) ⦃v : W⦄, v ∈ toSubmodule_1 → (ρ g) v ∈ toSubmodule_1},
  { toSubmodule := toSubmodule, apply_mem_toSubmodule := apply_mem_toSubmodule } =
      { toSubmodule := toSubmodule_1, apply_mem_toSubmodule := apply_mem_toSubmodule_1 } →
    toSubmodule = toSubmodule_1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.insert : ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Ineq.WithStrictness.lt.injEq : ∀ (strict strict_1 : Bool),
  (Mathlib.Ineq.WithStrictness.lt strict = Mathlib.Ineq.WithStrictness.lt strict_1) = (strict = strict_1)
-- Mathlib.Topology.DiscreteSubset
discreteTopology_subtype_iff : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] {S : Set Y},
  DiscreteTopology ↑S ↔ ∀ x ∈ S, nhdsWithin x {x}ᶜ ⊓ Filter.principal S = ⊥
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The product over `S ⊕ T` of a family of topological modules
is isomorphic (topologically and algebraically) to the product of
(the product over `S`) and (the product over `T`).

This is `Equiv.sumPiEquivProdPi` as a `ContinuousLinearEquiv`.
 -/
ContinuousLinearEquiv.sumPiEquivProdPi : (R : Type u_9) →
  [inst : Semiring R] →
    (S : Type u_10) →
      (T : Type u_11) →
        (A : S ⊕ T → Type u_12) →
          [inst_1 : (st : S ⊕ T) → AddCommMonoid (A st)] →
            [inst_2 : (st : S ⊕ T) → Module R (A st)] →
              [inst_3 : (st : S ⊕ T) → TopologicalSpace (A st)] →
                ((st : S ⊕ T) → A st) ≃L[R] ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))
-- Init.Data.SInt.Lemmas
Int64.ofInt_le_iff_le : ∀ {a b : ℤ},
  Int64.minValue.toInt ≤ a →
    a ≤ Int64.maxValue.toInt →
      Int64.minValue.toInt ≤ b → b ≤ Int64.maxValue.toInt → (Int64.ofInt a ≤ Int64.ofInt b ↔ a ≤ b)
-- Lean.Elab.Tactic.Omega.OmegaM
Lean.Elab.Tactic.Omega.Context.mk.sizeOf_spec : ∀ (cfg : Lean.Meta.Omega.OmegaConfig), sizeOf { cfg := cfg } = 1 + sizeOf cfg
-- Mathlib.Data.Ordmap.Invariants
Ordnode.node4L.eq_2 : ∀ {α : Type u_1} (x : Ordnode α) (x_1 x_2 : α) (x_3 : Ordnode α),
  x.node4L x_1 Ordnode.nil x_2 x_3 = x.node3L x_1 Ordnode.nil x_2 x_3
-- Mathlib.Data.Set.Lattice
Set.iInter_union : ∀ {β : Type u_2} {ι : Sort u_5} (s : ι → Set β) (t : Set β), (⋂ i, s i) ∪ t = ⋂ i, s i ∪ t
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of the reverse direction of `indiscreteTopology_iff_forall_nnnorm_eq_zero`. -/
IndiscreteTopology.of_forall_nnnorm_eq_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], (∀ (x : E), ‖x‖₊ = 0) → IndiscreteTopology E
-- Mathlib.NumberTheory.LegendreSymbol.Basic
ZMod.mod_four_ne_three_of_sq_eq_neg_one : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {y : ZMod p}, y ^ 2 = -1 → p % 4 ≠ 3
-- Mathlib.GroupTheory.Finiteness
/-- An additive monoid is finitely generated if it is finitely generated as an additive submonoid of
itself.  -/
AddMonoid.FG : (M : Type u_3) → [AddMonoid M] → Prop
-- Init.Data.BitVec.Lemmas
BitVec.sle_eq_ule_of_msb_eq : ∀ {w : ℕ} {x y : BitVec w}, x.msb = y.msb → x.sle y = x.ule y
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstr.mk : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Meta.Grind.AC.DiseqCnstrProof → Lean.Meta.Grind.AC.DiseqCnstr
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.add_congr : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : Add α] [Lean.Grind.ToInt.Add α i]
  {a b : α} {a' b' : ℤ}, ↑a = a' → ↑b = b' → ↑(a + b) = i.wrap (a' + b')
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.instPartialOrder : PartialOrder YoungDiagram
-- Init.Data.String.Basic
String.Slice.utf8ByteSize_copy_eq_sub : ∀ {s : String.Slice}, s.copy.utf8ByteSize = s.endExclusive.offset.byteIdx - s.startInclusive.offset.byteIdx
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.comm : ∀ {α : Type u} {m₁ m₂ : Std.HashSet.Raw α}, m₁.Equiv m₂ ↔ m₂.Equiv m₁
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.decompId_p.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Idempotents.Karoubi C),
  P.decompId_p = { f := P.p, comm := ⋯ }
-- Mathlib.Data.Set.Image
Set.image_univ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, f '' Set.univ = Set.range f
-- Mathlib.Order.Std
LinearOrder.OfStdArgs.mk : {α : Type u_1} →
  (toPartialOrderArgs : PartialOrder.OfStdArgs α) →
    (isLinearOrder :
        autoParam
          (let this := toPartialOrderArgs.le;
          Std.IsLinearOrder α)
          LinearOrder.OfStdArgs.isLinearOrder._autoParam) →
      (decidableLE : autoParam (DecidableLE α) LinearOrder.OfStdArgs.decidableLE._autoParam) →
        (decidableEq :
            autoParam
              (let this := toPartialOrderArgs;
              let this := decidableLE;
              DecidableEq α)
              LinearOrder.OfStdArgs.decidableEq._autoParam) →
          (decidableLT :
              autoParam
                (let this := toPartialOrderArgs.toPreorderArgs;
                let this := decidableLE;
                DecidableLT α)
                LinearOrder.OfStdArgs.decidableLT._autoParam) →
            (min :
                autoParam
                  (let this := toPartialOrderArgs.le;
                  let this := decidableLE;
                  Min α)
                  LinearOrder.OfStdArgs.min._autoParam) →
              (max :
                  autoParam
                    (let this := toPartialOrderArgs.le;
                    let this := decidableLE;
                    Max α)
                    LinearOrder.OfStdArgs.max._autoParam) →
                autoParam (Std.LawfulOrderLeftLeaningMin α) LinearOrder.OfStdArgs.lawfulOrderLeftLeaningMin._autoParam →
                  autoParam (Std.LawfulOrderLeftLeaningMax α)
                      LinearOrder.OfStdArgs.lawfulOrderLeftLeaningMax._autoParam →
                    (ord :
                        autoParam
                          (let this := toPartialOrderArgs.lt;
                          let this := decidableEq;
                          let this := decidableLT;
                          Ord α)
                          LinearOrder.OfStdArgs.ord._autoParam) →
                      autoParam
                          (let this := toPartialOrderArgs.le;
                          let this_1 := toPartialOrderArgs.lt;
                          let this_2 := ⋯;
                          let this_3 := isLinearOrder;
                          let this_4 := decidableEq;
                          let this_5 := decidableLT;
                          Std.LawfulOrderOrd α)
                          LinearOrder.OfStdArgs.lawfulOrderOrd._autoParam →
                        LinearOrder.OfStdArgs α
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.ext : ∀ {N : Type u_1} {G : Type u_2} {inst : Group N} {inst_1 : Group G} {φ : G →* MulAut N} {x y : N ⋊[φ] G},
  x.left = y.left → x.right = y.right → x = y
-- Aesop.Tree.TreeM
Aesop.TreeM.Context.mk : Aesop.Iteration → Aesop.LocalRuleSet → Aesop.TreeM.Context
-- Mathlib.Algebra.GroupWithZero.Commute
Ring.mul_inverse_rev : ∀ {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] (a b : M₀), Ring.inverse (a * b) = Ring.inverse b * Ring.inverse a
-- Mathlib.Analysis.Convex.Basic
convex_iff_forall_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E},
  Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s