mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.IsFormallyReal
IsFormallyReal.instOfIsStrictOrderedRing : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R], IsFormallyReal R
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.Pos.skipWhile.match_1.splitter : {s : String.Slice} →
  (motive : Option s.Pos → Sort u_1) →
    (x : Option s.Pos) → ((nextCurr : s.Pos) → motive (some nextCurr)) → (Unit → motive none) → motive x
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.of_finite : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  [Finite β] [L.HasSupport] {f : β → α}, Summable f L
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.mk.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  {W : C} (b : W ⟶ X) (π : (i : ι) → W ⟶ Y i) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (π i) (f i) = b),
  CategoryTheory.Limits.WidePullbackCone.mk b π h = CategoryTheory.Limits.WidePullbackShape.mkCone b π h
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItem.textEdit? : Lean.Lsp.CompletionItem → Option Lean.Lsp.InsertReplaceEdit
-- Mathlib.Algebra.GCDMonoid.Basic
/-- The greatest common divisor between two elements.  -/
GCDMonoid.gcd : {α : Type u_2} → {inst : CommMonoidWithZero α} → [self : GCDMonoid α] → α → α → α
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isBounded_of_abs_lt : ∀ {α : Type u_3} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [inst_3 : PseudoMetricSpace α]
  [CompactIccSpace α] (C : α), Bornology.IsBounded {x | |x| < C}
-- Mathlib.FieldTheory.AbelRuffini
/-- An induction principle for `solvableByRad`.  -/
solvableByRad.induction : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  (motive : (x : E) → x ∈ solvableByRad F E → Prop),
  (∀ (x : F), motive ((algebraMap F E) x) ⋯) →
    (∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E),
        motive x hx → motive y hy → motive (x + y) ⋯) →
      (∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E),
          motive x hx → motive y hy → motive (x * y) ⋯) →
        (∀ (n : ℕ) (x : E) (hn : n ≠ 0) (hx : x ^ n ∈ solvableByRad F E), motive (x ^ n) hx → motive x ⋯) →
          ∀ {x : E} (hx : x ∈ solvableByRad F E), motive x hx
-- Mathlib.Data.Rel.Separated
SetRel.isSeparated_insert' : ∀ {X : Type u_1} {R : SetRel X X} {s : Set X} {x : X},
  R.IsSeparated (insert x s) ↔ R.IsSeparated s ∧ (∀ y ∈ s, (x, y) ∈ R → x = y) ∧ ∀ y ∈ s, (y, x) ∈ R → x = y
-- Mathlib.Topology.Algebra.Ring.Basic
instSeparatelyContinuousMulAddOpposite : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst_1 : TopologicalSpace R] [SeparatelyContinuousMul R],
  SeparatelyContinuousMul Rᵃᵒᵖ
-- Mathlib.Data.Int.Cast.Defs
/-- An `AddCommGroupWithOne` is an `AddGroupWithOne` satisfying `a + b = b + a`.  -/
AddCommGroupWithOne : Type u → Type u
-- Mathlib.Topology.MetricSpace.Bounded
Metric.mem_cocompact_iff_closedBall_compl_subset : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α] [ProperSpace α] (c : α),
  s ∈ Filter.cocompact α ↔ ∃ r, (Metric.closedBall c r)ᶜ ⊆ s
-- Mathlib.RingTheory.SurjectiveOnStalks
/-- `R_p →+* S_q` is surjective if and only if
every `x : S` is of the form `f x / f r` for some `f r ∉ q`.
This is useful when proving `SurjectiveOnStalks`.
 -/
RingHom.surjective_localRingHom_iff : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S} (P : Ideal S)
  [inst_2 : P.IsPrime],
  Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) ↔
    ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.instSubHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M₁ M₂ : PresheafOfModules R} → Sub (M₁ ⟶ M₂)
-- Mathlib.Tactic.NormNum.IsSquare
/-- If `m ^ 2 < n < (m + 1) ^ 2`, then `n` is not a square.
We write this condition as `k < n ≤ k + 2 * m`, where `k = m * m`.  -/
Mathlib.Meta.NormNum.not_isSquare_nat_of_isNat : ∀ (a n : ℕ),
  Mathlib.Meta.NormNum.IsNat a n → ∀ (m k : ℕ), m * m = k → k.blt n = true → n.ble (k + 2 * m) = true → ¬IsSquare a
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.basisSets_singleton_mem : ∀ {R : Type u_1} {E : Type u_6} {ι : Type u_9} [inst : SeminormedRing R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (p : SeminormFamily R E ι) (i : ι) {r : ℝ}, 0 < r → (p i).ball 0 r ∈ p.basisSets
-- Mathlib.Data.Int.Init
Int.div_dvd_iff_dvd_mul : ∀ {a b c : ℤ}, b ∣ a → b ≠ 0 → (a / b ∣ c ↔ a ∣ b * c)
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd_apply : ∀ {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (x : CategoryTheory.Limits.Types.PullbackObj f g),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv) x) =
    (↑x).2
-- Init.Notation
/-- `tactic` is the builtin syntax category for tactics. These appear after
`by` in proofs, and they are programs that take in the proof context
(the hypotheses in scope plus the type of the term to synthesize) and construct
a term of the expected type. For example, `simp` is a tactic, used in:
```
example : 2 + 2 = 4 := by simp
```
 -/
Lean.Parser.Category.tactic : Lean.Parser.Category
-- Mathlib.Data.ENNReal.Real
ENNReal.dichotomy : ∀ (p : ENNReal) [Fact (1 ≤ p)], p = ⊤ ∨ 1 ≤ p.toReal
-- Mathlib.Algebra.Ring.NonZeroDivisors
dvd_cancel_right_coe_nonZeroDivisors : ∀ {R : Type u_1} [inst : CommRing R] {x y : R} {c : ↥(nonZeroDivisors R)}, x * ↑c ∣ y * ↑c ↔ x ∣ y
-- Mathlib.Algebra.Regular.SMul
/-- An element of `S` admitting a left inverse in `R` is `M`-regular.  -/
IsSMulRegular.of_smul_eq_one : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} {s : S} [inst : Monoid S] [inst_1 : SMul R M] [inst_2 : SMul R S]
  [inst_3 : MulAction S M] [IsScalarTower R S M], a • s = 1 → IsSMulRegular M s
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] {p : CategoryTheory.Functor N C}
  [inst_3 : CategoryTheory.InitiallySmall N] {U : N} {X : C} (f : p.obj U ⟶ X),
  CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk f =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.colimit.ι (p.op.comp (CategoryTheory.shrinkYoneda.{w, v, u}.obj X)) (Opposite.op U)))
      (CategoryTheory.shrinkYonedaObjObjEquiv.symm f)
-- Mathlib.NumberTheory.NumberField.AdeleRing
/-- The subgroup of principal adeles `(x)ᵥ` where `x ∈ K`.  -/
NumberField.AdeleRing.principalSubgroup : (R : Type u_1) →
  (K : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : IsDedekindDomain R] →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [inst_4 : IsFractionRing R K] → AddSubgroup (NumberField.AdeleRing R K)
-- Mathlib.MeasureTheory.Group.Arithmetic
Pi.measurableDiv₂ : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → Div (α i)] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  [∀ (i : ι), MeasurableDiv₂ (α i)], MeasurableDiv₂ ((i : ι) → α i)
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.instIteratorIdSearchStep.match_1.eq_2 : ∀ (s : String.Slice) (motive : String.Slice.Pattern.ForwardSliceSearcher s → Sort u_1) (pos : s.Pos)
  (h : pos ≠ s.endPos) (h_1 : (pos : s.Pos) → motive (String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos))
  (h_2 : (pos : s.Pos) → (h : pos ≠ s.endPos) → motive (String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h))
  (h_3 :
    (needle : String.Slice) →
      (table : Vector ℕ needle.utf8ByteSize) →
        (ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle) →
          (stackPos needlePos : String.Pos.Raw) →
            (hn : needlePos < needle.rawEndPos) →
              motive (String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn))
  (h_4 : Unit → motive String.Slice.Pattern.ForwardSliceSearcher.atEnd),
  (match String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h with
    | String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos => h_1 pos
    | String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h => h_2 pos h
    | String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn =>
      h_3 needle table ht stackPos needlePos hn
    | String.Slice.Pattern.ForwardSliceSearcher.atEnd => h_4 ()) =
    h_2 pos h
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_lt_ofReal_iff : ∀ {p q : ℝ}, 0 < q → (ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceNatCast' : Lean.Meta.Simp.DSimproc
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H1Iso.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.H1Iso A =
    (HomologicalComplex.sc (groupHomology.inhomogeneousChains A) 1).leftHomologyIso.symm ≪≫
      CategoryTheory.ShortComplex.leftHomologyMapIso' (groupHomology.isoShortComplexH1 A)
        (HomologicalComplex.sc (groupHomology.inhomogeneousChains A) 1).leftHomologyData
        (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM0.step.match_5.splitter : {Γ : Type u_1} →
  {Λ : Type u_2} →
    [inst : Inhabited Γ] →
      (motive : Turing.TM0.Cfg Γ Λ → Sort u_3) →
        (x : Turing.TM0.Cfg Γ Λ) → ((q : Λ) → (T : Turing.Tape Γ) → motive { q := q, Tape := T }) → motive x
-- Mathlib.CategoryTheory.Filtered.Basic
/-- An arbitrary choice of cocone over `F : J ⥤ C`, for `FinCategory J` and `IsFiltered C`.
 -/
CategoryTheory.IsFiltered.cocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsFiltered C] →
      {J : Type w} →
        [inst_2 : CategoryTheory.SmallCategory J] →
          [CategoryTheory.FinCategory J] → (F : CategoryTheory.Functor J C) → CategoryTheory.Limits.Cocone F
-- Mathlib.Topology.Sober
genericPoint_spec : ∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : QuasiSober α] [inst_2 : IrreducibleSpace α],
  IsGenericPoint (genericPoint α) Set.univ
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.mk.inj : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {inst : P.IsStableUnderBaseChange}
  {S : AlgebraicGeometry.Scheme} {J : Type u_1} {inst_1 : CategoryTheory.Category.{v_1, u_1} J}
  {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} {inst_2 : CategoryTheory.Category.{v_3, u_2} 𝒰.I₀}
  {inst_3 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰}
  {cocone :
    (i : 𝒰.I₀) → CategoryTheory.Limits.Cocone (D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)))}
  {isColimit : (i : 𝒰.I₀) → CategoryTheory.Limits.IsColimit (cocone i)}
  {prop_trans : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij)}
  {cocone_1 :
    (i : 𝒰.I₀) → CategoryTheory.Limits.Cocone (D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)))}
  {isColimit_1 : (i : 𝒰.I₀) → CategoryTheory.Limits.IsColimit (cocone_1 i)}
  {prop_trans_1 : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij)},
  { cocone := cocone, isColimit := isColimit, prop_trans := prop_trans } =
      { cocone := cocone_1, isColimit := isColimit_1, prop_trans := prop_trans_1 } →
    cocone = cocone_1 ∧ isColimit ≍ isColimit_1
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryLaxFunctor B C) (X : B), self.mapId X = CategoryTheory.eqToHom ⋯
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.instOfIsOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f], AlgebraicGeometry.IsPreimmersion f
-- Mathlib.CategoryTheory.GlueData
/-- If `F` preserves the gluing, and reflects the pullback of `U i ⟶ glued` and `U j ⟶ glued`,
then `F` reflects the fact that `V_pullback_cone` is a pullback.  -/
CategoryTheory.GlueData.vPullbackConeIsLimitOfMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    {C' : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v, u₂} C'] →
        (D : CategoryTheory.GlueData C) →
          (F : CategoryTheory.Functor C C') →
            [inst_2 : CategoryTheory.Limits.HasMulticoequalizer D.diagram] →
              [inst_3 : CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] →
                [inst_4 :
                    ∀ (i j k : D.J),
                      CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] →
                  (i j : D.J) →
                    [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan (D.ι i) (D.ι j)) F] →
                      CategoryTheory.Limits.IsLimit ((D.mapGlueData F).vPullbackCone i j) →
                        CategoryTheory.Limits.IsLimit (D.vPullbackCone i j)
-- Mathlib.Data.DFinsupp.Module
DFinsupp.distribMulAction₂ : {ι : Type u} →
  {γ : Type w} →
    {α : ι → Type u_2} →
      {δ : (i : ι) → α i → Type v} →
        [inst : Monoid γ] →
          [inst_1 : (i : ι) → (j : α i) → AddMonoid (δ i j)] →
            [(i : ι) → (j : α i) → DistribMulAction γ (δ i j)] → DistribMulAction γ (Π₀ (i : ι) (j : α i), δ i j)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.sup_le : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : SemilatticeSup β] [inst_3 : ContinuousSup β] (f g f' : α →ₘ[μ] β), f ≤ f' → g ≤ f' → f ⊔ g ≤ f'
-- Mathlib.Data.Set.Lattice
Set.biInter_ge : ∀ {α : Type u_1} {ι : Type u_12} [inst : PartialOrder ι] (s : ι → Set α) (i : ι),
  ⋂ j, ⋂ (_ : j ≥ i), s j = s i ∩ ⋂ j, ⋂ (_ : j > i), s j
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
ModularGroup.coe_inj : ∀ (a b : Matrix.SpecialLinearGroup (Fin 2) ℤ), ModularGroup.coe a = ModularGroup.coe b ↔ a = b
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.instInhabitedConsumerNode.default : Lean.Meta.SynthInstance.ConsumerNode
-- Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
/-- The modular discriminant equals `(E₄³ - E₆²) / 1728`.  -/
ModularForm.discriminant_eq_E₄_cube_sub_E₆_sq : ∀ (z : UpperHalfPlane), ModularForm.discriminant z = (ModularForm.E₄ z ^ 3 - ModularForm.E₆ z ^ 2) / 1728
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.refl_h : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : SSet.RelativeMorphism A B φ),
  (SSet.RelativeMorphism.Homotopy.refl f).h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X (SSet.stdSimplex.obj { len := 1 })) f.map
-- Std.Time.Date.Basic
/-- Convert `Day.Offset` into `Minute.Offset`.
 -/
Std.Time.Minute.Offset.ofDays : Std.Time.Day.Offset → Std.Time.Minute.Offset
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.ins.match_3.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α)
  (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 : (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a y b))
  (h_3 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b)),
  (match RBTree.RBNode.node RBTree.RBColor.black a y b with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node RBTree.RBColor.red a y b => h_2 a y b
    | RBTree.RBNode.node RBTree.RBColor.black a y b => h_3 a y b) =
    h_3 a y b
-- Init.Data.Array.Lemmas
Array.getElem?_eq_getElem : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size), xs[i]? = some xs[i]
-- Std.Http.Data.Headers.Value
Std.Http.Header.Value.instToString : ToString Std.Http.Header.Value
-- Mathlib.Order.Hom.BoundedLattice
/-- Composition of `InfTopHom`s as an `InfTopHom`.  -/
InfTopHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Min α] →
        [inst_1 : Top α] →
          [inst_2 : Min β] →
            [inst_3 : Top β] → [inst_4 : Min γ] → [inst_5 : Top γ] → InfTopHom β γ → InfTopHom α β → InfTopHom α γ
-- Mathlib.Algebra.Order.Antidiag.Nat
_private.Mathlib.Algebra.Order.Antidiag.Nat.0.Nat.card_pair_lcm_eq.f_img : ∀ {n : ℕ},
  Squarefree n →
    ∀ (a : Fin 3 → ℕ) (ha : a ∈ Nat.finMulAntidiag 3 n),
      Nat.card_pair_lcm_eq.f✝ a ha ∈
        {x ∈ n.divisors ×ˢ n.divisors |
          match x with
          | (x, y) => x.lcm y = n}
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.map_injective : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {f : A →ₐ[R] B},
  Function.Injective ⇑f → Function.Injective (Subalgebra.map f)
-- Init.Data.List.MinMax
List.max_eq_iff : ∀ {α : Type u_1} {a : α} [inst : Max α] [inst_1 : LE α] {l : List α} [Std.IsLinearOrder α] [Std.LawfulOrderMax α]
  (hl : l ≠ []), l.max hl = a ↔ a ∈ l ∧ ∀ b ∈ l, b ≤ a
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.support_nilradical : ∀ (X : AlgebraicGeometry.Scheme), X.nilradical.support = ⊤
-- Lean.Meta.Sym.SymM
/-- Returns the internalized `Int`.   -/
Lean.Meta.Sym.getIntExpr : Lean.Meta.Sym.SymM Lean.Expr
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedFieldInfo : Inhabited Lean.Elab.FieldInfo
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_eq_toArray_rco : ∀ {m n : ℕ}, (m<...n).toArray = ((m + 1)...n).toArray
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.pos : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 < p
-- Mathlib.Control.Applicative
Applicative.pure_seq_eq_map' : ∀ {F : Type u → Type v} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → β),
  (fun x => pure f <*> x) = fun x => f <$> x
-- Mathlib.RingTheory.WittVector.Basic
WittVector.map_eq_zero_iff : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S) {x : WittVector p R}, (WittVector.map f) x = 0 ↔ ∀ (n : ℕ), f (x.coeff n) = 0
-- Mathlib.Order.Category.BddOrd
BddOrd.Hom.ext_iff : ∀ {X Y : BddOrd} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Topology.ContinuousMap.Basic
/-- `Set.inclusion` as a bundled continuous map.  -/
ContinuousMap.inclusion : {α : Type u_1} → [inst : TopologicalSpace α] → {s t : Set α} → s ⊆ t → C(↑s, ↑t)
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Header.mk.injEq : ∀ (binders : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) (argNames targetNames : Array Lean.Name)
  (targetType : Lean.Term) (binders_1 : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder))
  (argNames_1 targetNames_1 : Array Lean.Name) (targetType_1 : Lean.Term),
  ({ binders := binders, argNames := argNames, targetNames := targetNames, targetType := targetType } =
      { binders := binders_1, argNames := argNames_1, targetNames := targetNames_1, targetType := targetType_1 }) =
    (binders = binders_1 ∧ argNames = argNames_1 ∧ targetNames = targetNames_1 ∧ targetType = targetType_1)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.reverse_mul : ∀ {α : Type u_1} {a b : FreeMonoid α}, (a * b).reverse = b.reverse * a.reverse
-- Mathlib.GroupTheory.Torsion
CommMonoid.torsion_prod : ∀ (G : Type u_1) {H : Type u_2} [inst : CommMonoid G] [inst_1 : CommMonoid H],
  CommMonoid.torsion (G × H) = (CommMonoid.torsion G).prod (CommMonoid.torsion H)
-- Init.Data.Bool
Bool.decide_false_eq : ∀ {b : Bool} [inst : Decidable (false = b)], decide (false = b) = !b
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
CategoryTheory.Limits.colim.mapShortComplex_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
  {c₁ : CategoryTheory.Limits.Cocone S.X₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁)
  (c₂ : CategoryTheory.Limits.Cocone S.X₂) (c₃ : CategoryTheory.Limits.Cocone S.X₃) (f : c₁.pt ⟶ c₂.pt)
  (g : c₂.pt ⟶ c₃.pt)
  (hf :
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (c₁.ι.app j) f = CategoryTheory.CategoryStruct.comp (S.f.app j) (c₂.ι.app j))
  (hg :
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (c₂.ι.app j) g = CategoryTheory.CategoryStruct.comp (S.g.app j) (c₃.ι.app j)),
  (CategoryTheory.Limits.colim.mapShortComplex S hc₁ c₂ c₃ f g hf hg).X₁ = c₁.pt
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} (b : β),
  s +ᵥ {b} = Finset.image (fun x => x +ᵥ b) s
-- Mathlib.FieldTheory.Separable
Associated.separable : ∀ {R : Type u} [inst : CommSemiring R] {f g : Polynomial R}, Associated f g → f.Separable → g.Separable
-- Mathlib.Tactic.RenameBVar
/-- Renames a bound variable in a hypothesis.  -/
Mathlib.Tactic.renameBVarHyp : Lean.MVarId → Lean.FVarId → Lean.Name → Lean.Name → Lean.MetaM Unit
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeFunctorPreservesFiniteLimitsOfHasExactColimitsOfShape : ∀ {J : Type u_1} {C : Type u_3} (K' : Type u_6) [inst : CategoryTheory.Category.{v_2, u_6} K']
  [inst_1 : CategoryTheory.Category.{v_3, u_1} J] [inst_2 : CategoryTheory.Category.{v_5, u_3} C]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K' C] [CategoryTheory.HasExactColimitsOfShape K' C],
  CategoryTheory.ObjectProperty.preservesFiniteLimits.IsClosedUnderColimitsOfShape K'
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.AllZero.nil : Tactic.ComputeAsymptotics.UnitMonomial.AllZero []
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_zsmul : ∀ {ι : Type u_1} {G : Type u_5} [inst : SubtractionCommMonoid G] (f : ι → G) (s : Finset ι) (n : ℤ),
  ∑ a ∈ s, n • f a = n • ∑ a ∈ s, f a
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.den_natCast : ∀ {m : Type u_1} [inst : Fintype m] [inst_1 : DecidableEq m] (a : ℕ), (↑a).den = 1
-- Lean.Elab.Command
/-- Adapt a syntax transformation to a regular, command-producing elaborator.  -/
Lean.Elab.Command.adaptExpander : (Lean.Syntax → Lean.Elab.Command.CommandElabM Lean.Syntax) → Lean.Elab.Command.CommandElab
-- Mathlib.CategoryTheory.Comma.Arrow
/-- A variant of `Arrow.isoMk` that creates an iso between two `Arrow.mk`s with a better type
signature.  -/
CategoryTheory.Arrow.isoMk' : {T : Type u} →
  [inst : CategoryTheory.Category.{v, u} T] →
    {W X Y Z : T} →
      (f : W ⟶ X) →
        (g : Y ⟶ Z) →
          (e₁ : W ≅ Y) →
            (e₂ : X ≅ Z) →
              autoParam (CategoryTheory.CategoryStruct.comp e₁.hom g = CategoryTheory.CategoryStruct.comp f e₂.hom)
                  CategoryTheory.Arrow.isoMk'._auto_1 →
                (CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g)
-- Mathlib.Topology.Connected.PathConnected
Submonoid.pathComponentOne.congr_simp : ∀ (M : Type u_4) [inst : Monoid M] [inst_1 : TopologicalSpace M] [inst_2 : ContinuousMul M],
  Submonoid.pathComponentOne M = Submonoid.pathComponentOne M
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_fiberwise' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq κ] [inst_2 : Fintype κ]
  (s : Finset ι) (g : ι → κ) (f : κ → M), ∏ j, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s, f (g i)