mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.instStrongMonoOfIsRegularMono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsRegularMono f],
  CategoryTheory.StrongMono f
-- Mathlib.Algebra.Ring.CompTypeclasses
/-- Class that expresses that a ring homomorphism is in fact the identity.  -/
RingHomId : {R : Type u_4} → [inst : Semiring R] → (R →+* R) → Prop
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The `ℤ`-linear map induced by precomposition of the projection
`π C (ord I · < o₂) → π C (ord I · < o₁)` for `o₁ ≤ o₂`.  -/
Profinite.NobelingProof.πs' : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        {o₁ o₂ : Ordinal.{u}} →
          o₁ ≤ o₂ →
            LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₁) ℤ →ₗ[ℤ]
              LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₂) ℤ
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.image_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} (H : Hypergraph α),
  (H.image f).image g = H.image (g ∘ f)
-- Mathlib.Data.Finset.Erase
Finset.mem_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {s : Finset α}, a ∈ s.erase b ↔ a ≠ b ∧ a ∈ s
-- Mathlib.Data.Complex.Basic
Complex.normSq_pos : ∀ {z : ℂ}, 0 < Complex.normSq z ↔ z ≠ 0
-- Mathlib.RingTheory.NoetherNormalization
/-- We construct an algebra map `T1 f c` which maps `X_i` into `X_i + c • X_0 ^ r_i` when `i ≠ 0`
and `X_0` to `X_0`.  -/
NoetherNormalization.T1 : {k : Type u_1} →
  [inst : Field k] →
    {n : ℕ} → MvPolynomial (Fin (n + 1)) k → k → MvPolynomial (Fin (n + 1)) k →ₐ[k] MvPolynomial (Fin (n + 1)) k
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_comap_eq : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup N),
  AddSubgroup.map f (AddSubgroup.comap f H) = f.range ⊓ H
-- Init.Data.SInt.Lemmas
Int64.toInt_div : ∀ (a b : Int64), (a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ 64)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.bin.inj : ∀ {w : ℕ} {lhs : Std.Tactic.BVDecide.BVExpr w} {op : Std.Tactic.BVDecide.BVBinOp}
  {rhs lhs_1 : Std.Tactic.BVDecide.BVExpr w} {op_1 : Std.Tactic.BVDecide.BVBinOp}
  {rhs_1 : Std.Tactic.BVDecide.BVExpr w}, lhs.bin op rhs = lhs_1.bin op_1 rhs_1 → lhs = lhs_1 ∧ op = op_1 ∧ rhs = rhs_1
-- Mathlib.Order.SuccPred.Basic
/-- See also `Order.pred_le_of_wcovBy`.  -/
Order.pred_eq_of_covBy : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a b : α}, b ⋖ a → Order.pred a = b
-- Mathlib.Data.NNRat.Defs
NNRat.coe_mono : Monotone NNRat.cast
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_mul_aleph0 : ∀ {m : ℕ∞}, m ≠ 0 → ↑m * Cardinal.aleph0 = Cardinal.aleph0
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.specOrderIsoPrimeSpectrum_symm_apply : ∀ (R : CommRingCat) (x : (PrimeSpectrum ↑R)ᵒᵈ),
  (RelIso.symm (AlgebraicGeometry.specOrderIsoPrimeSpectrum R)) x = OrderDual.ofDual x
-- Mathlib.CategoryTheory.Shift.SingleFunctorsLift
/-- Auxiliary definition for `SingleFunctors.lift`.  -/
CategoryTheory.SingleFunctors.lift.shiftIso : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{u_5, u_1} C] →
        [inst_1 : CategoryTheory.Category.{u_6, u_2} D] →
          [inst_2 : CategoryTheory.Category.{u_7, u_3} E] →
            {A : Type u_4} →
              [inst_3 : AddMonoid A] →
                [inst_4 : CategoryTheory.HasShift D A] →
                  [inst_5 : CategoryTheory.HasShift E A] →
                    {F : CategoryTheory.SingleFunctors C E A} →
                      {G : CategoryTheory.Functor D E} →
                        [G.CommShift A] →
                          [G.Full] →
                            [G.Faithful] →
                              {Φ : A → CategoryTheory.Functor C D} →
                                ((a : A) → (Φ a).comp G ≅ F.functor a) →
                                  (n a a' : A) → n + a = a' → ((Φ a').comp (CategoryTheory.shiftFunctor D n) ≅ Φ a)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rcc_eq_some_iff : ∀ {k m n i : ℕ}, (m...=n).toArray[i]? = some k ↔ i < n + 1 - m ∧ m + i = k
-- Mathlib.Data.Num.Basic
instReprPosNum : Repr PosNum
-- Mathlib.Algebra.Homology.DerivedCategory.KProjective
CochainComplex.IsKProjective.quasiIso_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {K L : CochainComplex C ℤ}
  [K.IsKProjective] [L.IsKProjective] (f : K ⟶ L),
  QuasiIso f ↔ HomologicalComplex.homotopyEquivalences C (ComplexShape.up ℤ) f
-- Init.Data.Range.Polymorphic.PRange
Std.Rco.instDecidableMemOfDecidableLEOfDecidableLT : {α : Type u} →
  {r : Std.Rco α} → {a : α} → [inst : LE α] → [DecidableLE α] → [inst_2 : LT α] → [DecidableLT α] → Decidable (a ∈ r)
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
CategoryTheory.Sieve.effectiveEpimorphic_singleton : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : Y ⟶ X),
  (CategoryTheory.Presieve.singleton f).EffectiveEpimorphic ↔ CategoryTheory.EffectiveEpi f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp},
  t₁.Equiv t₂ → ∀ (f : (a : α) → β a → Bool), (Std.DTreeMap.filter f t₁).Equiv (Std.DTreeMap.filter f t₂)
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.toTop_obj_carrier : ∀ (R : CommRingCatᵒᵖ), ↑(AlgebraicGeometry.Spec.toTop.obj R) = PrimeSpectrum ↑(Opposite.unop R)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.preimage_coe_affineSpan_singleton : ∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (x : P), Subtype.val ⁻¹' {x} = Set.univ
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iic_top : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : OrderTop α] [inst_3 : Fintype α],
  Finset.Iic ⊤ = Finset.univ
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.toList_succ_succ_eq_map : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.InfinitelyUpwardEnumerable α] [inst_6 : Std.Rxc.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {lo hi : α},
  ((Std.PRange.succ lo)...=Std.PRange.succ hi).toList = List.map Std.PRange.succ (lo...=hi).toList
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.negRev.eq_1 : ∀ {α : Type u} (w : List (α × Bool)), FreeAddGroup.negRev w = (List.map (fun g => (g.1, !g.2)) w).reverse
-- Lean.Util.ForEachExprWhere
/-- `Expr.forEachWhere` (unsafe) implementation  -/
Lean.ForEachExprWhere.visit : {ω : Type} →
  {m : Type → Type} →
    [STWorld ω m] →
      [MonadLiftT (ST ω) m] →
        [Monad m] → (Lean.Expr → Bool) → (Lean.Expr → m Unit) → Lean.Expr → optParam Bool false → m Unit
-- Init.Data.List.Lemmas
/-- Variant of `map_id`, with a side condition that the function is pointwise the identity.  -/
List.map_id'' : ∀ {α : Type u_1} {f : α → α}, (∀ (x : α), f x = x) → ∀ (l : List α), List.map f l = l
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.embDomain.eq_1 : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  (f : Γ ↪o Γ') (x : HahnSeries Γ R),
  HahnSeries.embDomain f x =
    { coeff := fun b => if h : b ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0, isPWO_support' := ⋯ }
-- Mathlib.Topology.Spectral.Hom
SpectralMapClass.toContinuousMapClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : FunLike F α β] [SpectralMapClass F α β], ContinuousMapClass F α β
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.nilRank_le_card : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup L] [inst_2 : Module R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M) [inst_5 : Module.Free R M]
  [inst_6 : Module.Finite R M] [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] [Nontrivial R] {ι : Type u_8}
  [inst_10 : Fintype ι] (b : Module.Basis ι R M), φ.nilRank ≤ Fintype.card ι
-- Mathlib.Algebra.BigOperators.Finprod
/-- If `R` has no zero divisors, then multiplication commutes with finsums. See `finsum_mul'` for a
statement assuming finiteness of support.
 -/
finsum_mul : ∀ {α : Type u_1} {R : Type u_7} [inst : NonUnitalNonAssocSemiring R] [NoZeroDivisors R] (f : α → R) (r : R),
  (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Radon-Nikodym derivative of the scalar multiple of a measure.
See also `rnDeriv_smul_left'`, which requires sigma-finite `ν` and `μ`.  -/
MeasureTheory.Measure.rnDeriv_smul_left : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν]
  [ν.HaveLebesgueDecomposition μ] (r : NNReal), (r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ
-- Mathlib.Analysis.Convex.Segment
/-- A point is in an `Ioo` iff it can be expressed as a strict convex combination of the endpoints.
 -/
Convex.mem_Ioo : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y z : 𝕜},
  x < y → (z ∈ Set.Ioo x y ↔ ∃ a b, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z)
-- Lean.Elab.DocString
/-- More information to show users  -/
Lean.Doc.CodeBlockSuggestion.moreInfo : Lean.Doc.CodeBlockSuggestion → Option String
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.one_lt_mul_of_lt_of_le`.

---

Assumes left covariance.
The lemma assuming right covariance is `Right.one_lt_mul_of_lt_of_le`.  -/
one_lt_mul_of_lt_of_le' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b : α}, 1 < a → 1 ≤ b → 1 < a * b
-- Mathlib.Topology.Separation.CompletelyRegular
instCompletelyRegularSpaceProd : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [htX : CompletelyRegularSpace X]
  [htY : CompletelyRegularSpace Y], CompletelyRegularSpace (X × Y)
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] (f : BoundedLatticeHom β γ)
  (g : BoundedLatticeHom α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
GenContFract.of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K} {n : ℕ},
  (GenContFract.of v).TerminatedAt n ↔ GenContFract.IntFractPair.stream v (n + 1) = none
-- Std.Data.HashSet.Raw
/-- Two hash sets are equivalent in the sense of `Equiv` iff all their values are equal.
 -/
Std.HashSet.Raw.Equiv : {α : Type u} → Std.HashSet.Raw α → Std.HashSet.Raw α → Prop
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.instIsLowerProd : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α] [OrderBot α]
  [inst_4 : Preorder β] [inst_5 : TopologicalSpace β] [Topology.IsLower β] [OrderBot β], Topology.IsLower (α × β)
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.single_op : ∀ {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} [inst : (i : ι) → Zero (M i)] [inst_1 : (i : ι) → Zero (N i)]
  [inst_2 : DecidableEq ι] (op : (i : ι) → M i → N i),
  (∀ (i : ι), op i 0 = 0) → ∀ (i : ι) (x : M i), Pi.single i (op i x) = fun j => op j (Pi.single i x j)
-- Init.Data.SInt.Lemmas
Int8.le_antisymm_iff : ∀ {a b : Int8}, a = b ↔ a ≤ b ∧ b ≤ a
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₁_snd : ∀ (X : SSet),
  CategoryTheory.CategoryStruct.comp SSet.ι₁
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X (SSet.stdSimplex.obj { len := 1 })) =
    SSet.const (SSet.stdSimplex.obj₀Equiv.symm 1)
-- Mathlib.Data.Rel
Set.preimage_eq : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β), f ⁻¹' s = (Function.graph f).preimage s
-- Mathlib.Data.ENNReal.Basic
ENNReal.instCharZero : CharZero ENNReal
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.MutuallySingular.neg_left_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : TopologicalSpace N]
  {M : Type u_6} [inst_2 : AddCommGroup M] [inst_3 : TopologicalSpace M] [inst_4 : IsTopologicalAddGroup M]
  {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N},
  (-v).MutuallySingular w ↔ v.MutuallySingular w
-- Mathlib.CategoryTheory.EssentialImage
/-- Given an essentially surjective functor, we can find a preimage for every object `Y` in the
codomain. Applying the functor to this preimage will yield an object isomorphic to `Y`, see
`obj_obj_preimage_iso`.  -/
CategoryTheory.Functor.objPreimage : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (F : CategoryTheory.Functor C D) → [F.EssSurj] → D → C
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.hom_neg_apply : ∀ {X Y : AddCommGrpCat} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestImpl.evalSuggestCore : Lean.TSyntax `tactic → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Mathlib.Algebra.Lie.Basic
LieHom.comp_id : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂), f.comp LieHom.id = f
-- Mathlib.NumberTheory.ModularForms.DedekindEta
/-- Eta is non-vanishing on the upper half plane.  -/
ModularForm.eta_ne_zero : ∀ {z : ℂ}, z ∈ UpperHalfPlane.upperHalfPlaneSet → ModularForm.eta z ≠ 0
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.map_id_obj_unop : ∀ {X : TopCat} (x : ↑X) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ),
  (TopologicalSpace.OpenNhds.map (CategoryTheory.CategoryStruct.id X) x).obj (Opposite.unop U) = Opposite.unop U
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_d : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.up α)) (i j : α),
  ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.obj K).X.d i j = (K.d i j).f
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ⟶ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))
            (θ.naturality f).hom =
          CategoryTheory.CategoryStruct.comp (η.naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
      CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality._autoParam)
  (app_1 : (a : B) → η.app a ⟶ θ.app a)
  (naturality_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app_1 b))
            (θ.naturality f).hom =
          CategoryTheory.CategoryStruct.comp (η.naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (app_1 a) (G.map f)))
      CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality._autoParam),
  ({ app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 }) = (app = app_1)
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
/-- Simplification of the integral of `sin x ^ m * cos x ^ n`, case `m` and `n` are both even.  -/
integral_sin_pow_even_mul_cos_pow_even : ∀ {a b : ℝ} (m n : ℕ),
  ∫ (x : ℝ) in a..b, Real.sin x ^ (2 * m) * Real.cos x ^ (2 * n) =
    ∫ (x : ℝ) in a..b, ((1 - Real.cos (2 * x)) / 2) ^ m * ((1 + Real.cos (2 * x)) / 2) ^ n
-- Lean.Server.References
/-- Direct imports of the module that the file worker is associated with.  -/
Lean.Server.TransientWorkerILean.directImports : Lean.Server.TransientWorkerILean → Lean.Server.DirectImports
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.biSup_comap_subtype_eq_top : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_9}
  (s : Set ι) (p : ι → Submodule R M), ⨆ i ∈ s, Submodule.comap (⨆ i ∈ s, p i).subtype (p i) = ⊤
-- Init.Data.Array.Bootstrap
_private.Init.Data.Array.Bootstrap.0.Array.forIn'.loop.match_3.eq_1 : ∀ {α : Type u_1} (as : Array α) (motive : (i : ℕ) → i ≤ as.size → Sort u_2) (x : 0 ≤ as.size)
  (h_1 : (x : 0 ≤ as.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ as.size) → motive i.succ h),
  (match 0, x with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_1 x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).getKey! k = if (f (Std.DTreeMap.Const.get? t k)).isSome = true then k else default
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Turn an `Expr` into an HTML with hover info.  -/
Mathlib.Tactic.ClickSuggestions.exprToHtml : Lean.Expr → Lean.MetaM ProofWidgets.Html
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.subset_span : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {s : Set R}, s ⊆ ↑(TwoSidedIdeal.span s)
-- Mathlib.Analysis.Normed.Group.Basic
dist_eq_norm_neg_add' : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), dist a b = ‖-b + a‖
-- Mathlib.Data.Seq.Computation
Computation.LiftRel.trans : ∀ {α : Type u} (R : α → α → Prop) [IsTrans α R], IsTrans (Computation α) (Computation.LiftRel R)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpTriggerKind : Type
-- Mathlib.Algebra.Star.LinearMap
LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr : ∀ {R : Type u_5} {E : Type u_6} {F : Type u_7} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid E]
  [inst_3 : StarAddMonoid E] [inst_4 : Module R E] [inst_5 : StarModule R E] [inst_6 : AddCommMonoid F]
  [inst_7 : StarAddMonoid F] [inst_8 : Module R F] [inst_9 : StarModule R F],
  starLinearEquiv R =
    (WithConv.linearEquiv R (E →ₗ[R] F)).trans
      (((starLinearEquiv R).arrowCongr (starLinearEquiv R)).trans (WithConv.linearEquiv R (E →ₗ[R] F)).symm)
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_inter_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₂.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Mathlib.RingTheory.FinitePresentation
RingHom.FinitePresentation.id : ∀ (A : Type u_1) [inst : CommRing A], (RingHom.id A).FinitePresentation
-- Mathlib.Combinatorics.Enumerative.Stirling
_private.Mathlib.Combinatorics.Enumerative.Stirling.0.Nat.stirlingFirst.match_1.eq_3 : ∀ (motive : ℕ → ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0 0) (h_2 : (n : ℕ) → motive 0 n.succ)
  (h_3 : (n : ℕ) → motive n.succ 0) (h_4 : (n k : ℕ) → motive n.succ k.succ),
  (match n.succ, 0 with
    | 0, 0 => h_1 ()
    | 0, n.succ => h_2 n
    | n.succ, 0 => h_3 n
    | n.succ, k.succ => h_4 n k) =
    h_3 n
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.Hom.naturality_assoc : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {P Q : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D} (self : P.Hom Q) ⦃X X' : C⦄ ⦃Y Y' : D⦄ (f : X ⟶ X')
  (g : Y ⟶ Y') {Z : Type w} (h : Q.obj X' Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.map f g) (CategoryTheory.CategoryStruct.comp (self.app X' Y) h) =
    CategoryTheory.CategoryStruct.comp (self.app X Y') (CategoryTheory.CategoryStruct.comp (Q.map f g) h)
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.refl_apply : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) (x : ↑unitInterval × ↑unitInterval),
  (Path.Homotopy.refl p) x = p x.2
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.exp.eq_1 : ∀ {M : Type u_4} (a : M), WithZero.exp a = ↑(Multiplicative.ofAdd a)
-- Mathlib.Tactic.TermCongr
/-- Make a `CongrResult` from an LHS, an RHS, and a proof of an Iff, Eq, or HEq.
The proof is allowed to have a metavariable for its type.
Validates the inputs and throws errors in the `pf?` function.

The `pf?` function is responsible for finally unifying the type of `pf` with `lhs` and `rhs`.  -/
Mathlib.Tactic.TermCongr.CongrResult.mk' : Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Tactic.TermCongr.CongrResult
-- Mathlib.RepresentationTheory.Basic
Representation.IsTrivial.mk : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] {ρ : Representation k G V},
  autoParam (∀ (g : G), ρ g = LinearMap.id) Representation.IsTrivial.out._autoParam → ρ.IsTrivial
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.le_N : ∀ {N : ℕ}, 2 ≤ N → (2 * Behrend.dValue N - 1) ^ Behrend.nValue N ≤ N
-- Lean.Util.Trace
Lean.checkTraceOption : Std.HashSet Lean.Name → Lean.Options → Lean.Name → Bool
-- Init.Data.Int.Order
Int.lt_add_of_le_of_pos : ∀ {a b c : ℤ}, b ≤ c → 0 < a → b < c + a
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.lift_φ₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) {A : C} (a : A ⟶ S.L₁.X₂) (b : A ⟶ S.L₀.X₃)
  (h : CategoryTheory.CategoryStruct.comp a S.L₁.g = CategoryTheory.CategoryStruct.comp b S.v₀₁.τ₃) {Z : C}
  (h_1 : S.L₂.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift a b h)
      (CategoryTheory.CategoryStruct.comp S.φ₂ h_1) =
    CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp S.v₁₂.τ₂ h_1)
-- Mathlib.CategoryTheory.Triangulated.Generators
/-- All objects that can be reached by shifts, binary products, retracts and extensions
from objects in `P`. This is the smallest triangulated object property closed under retracts
that contains `P`, see `ObjectProperty.triangEnvelope_le_iff`.  -/
CategoryTheory.ObjectProperty.triangEnvelope : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [CategoryTheory.Pretriangulated C] → CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.toLower_le_toLower : ∀ {α : Type u_1} [inst : Preorder α] {x y : α}, Topology.WithLower.toLower x ≤ Topology.WithLower.toLower y ↔ x ≤ y
-- Mathlib.Order.Filter.NAry
Filter.map₂_neBot_iff : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β},
  (Filter.map₂ m f g).NeBot ↔ f.NeBot ∧ g.NeBot
-- Init.Data.Array.Attach
Array.attach_map_subtype_val : ∀ {α : Type u_1} (xs : Array α), Array.map Subtype.val xs.attach = xs
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_insertIfNew_le_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α} {v : β k}, (cmp (t.insertIfNew k v).minKey! t.minKey!).isLE = true
-- Mathlib.Algebra.Squarefree.Basic
Irreducible.squarefree : ∀ {R : Type u_1} [inst : CommMonoid R] {x : R}, Irreducible x → Squarefree x