mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Term
Lean.Parser.Term.letIdBinder.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.condition : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g),
  CategoryTheory.CategoryStruct.comp t.ι f = CategoryTheory.CategoryStruct.comp t.ι g
-- Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedUnopOfOpposite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty Cᵒᵖ) [P.IsTriangulated], P.unop.IsTriangulated
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- The Frobenius automorphism of `k` induces an endomorphism of `K`. For notation purposes.
Notation `φ(p, k)` in the `Isocrystal` namespace.  -/
WittVector.FractionRing.frobeniusRingHom : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (k : Type u_1) →
      [inst_1 : CommRing k] →
        [CharP k p] → [PerfectRing k p] → FractionRing (WittVector p k) →+* FractionRing (WittVector p k)
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_closure : ∀ {α : Type u} (M : Matroid α) [M.InvariantCardinalRank] (X : Set α), M.cRk (M.closure X) = M.cRk X
-- Lean.Elab.Arg
Lean.Elab.Term.Arg.expr.sizeOf_spec : ∀ (val : Lean.Expr), sizeOf (Lean.Elab.Term.Arg.expr val) = 1 + sizeOf val
-- Std.Do.SPred.SVal
/-- Uncurries an `SVal` into a function taking a `StateTuple`.  -/
Std.Do.SVal.uncurry : {α : Type u} → {σs : List (Type u)} → Std.Do.SVal σs α → Std.Do.SVal.StateTuple σs → α
-- Mathlib.Data.Nat.ChineseRemainder
Nat.chineseRemainderOfList_perm : ∀ {ι : Type u_1} (a s : ι → ℕ) {l l' : List ι} (hl : l.Perm l'),
  (∀ i ∈ l, s i ≠ 0) →
    ∀ (co : List.Pairwise (Function.onFun Nat.Coprime s) l),
      ↑(Nat.chineseRemainderOfList a s l co) = ↑(Nat.chineseRemainderOfList a s l' ⋯)
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppScalarLeft_apply_tmul_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_4} [inst_1 : AddCommMonoid N] [inst_2 : Module R N] {ι : Type u_5}
  [inst_3 : DecidableEq ι] (p : ι →₀ R) (n : N) (i : ι),
  ((TensorProduct.finsuppScalarLeft R N ι) (p ⊗ₜ[R] n)) i = p i • n
-- Init.Core
Std.Commutative.mk : ∀ {α : Sort u} {op : α → α → α}, (∀ (a b : α), op a b = op b a) → Std.Commutative op
-- Mathlib.Data.Fintype.BigOperators
Equiv.subtypeEquivRight.congr_simp : ∀ {α : Sort u_1} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x), Equiv.subtypeEquivRight e = Equiv.subtypeEquivRight e
-- Mathlib.Analysis.CStarAlgebra.Unitization
Unitization.instCommCStarAlgebra : {A : Type u_3} → [NonUnitalCommCStarAlgebra A] → CommCStarAlgebra (Unitization ℂ A)
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- The set of points that are covered by the union of balls selected at steps `< i`.  -/
Besicovitch.TauPackage.iUnionUpTo : {α : Type u_1} → [MetricSpace α] → {β : Type u} → [Nonempty β] → Besicovitch.TauPackage β α → Ordinal.{u} → Set α
-- Init.Data.Array.Find
Array.findIdx?_eq_findSome?_zipIdx : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool},
  Array.findIdx? p xs =
    Array.findSome?
      (fun x =>
        match x with
        | (a, i) => if p a = true then some i else none)
      xs.zipIdx
-- Mathlib.Order.Filter.Defs
Filter.inter_mem : ∀ {α : Type u_1} {f : Filter α} {s t : Set α}, s ∈ f → t ∈ f → s ∩ t ∈ f
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.apply_eq_iff_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (e : α ≃+o β) {x : α} {y : β}, e x = y ↔ x = e.symm y
-- Mathlib.Dynamics.Flow
Flow.continuous : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  (ϕ : Flow τ α) {β : Type u_3} [inst_3 : TopologicalSpace β] {t : β → τ},
  Continuous t → ∀ {f : β → α}, Continuous f → Continuous fun x => ϕ.toFun (t x) (f x)
-- Mathlib.Logic.Function.FromTypes
Function.fromTypes_cons_equiv_apply : ∀ {n : ℕ} (α : Type u) (p : Fin n → Type u) (τ : Type u) (a : Function.FromTypes (Matrix.vecCons α p) τ),
  (Function.fromTypes_cons_equiv α p τ) a = a
-- Mathlib.GroupTheory.FiniteAbelian.Duality
/-- If `G` is a finite commutative group of exponent `n` and `M` is a commutative monoid
with enough `n`th roots of unity, then for each `a ≠ 1` in `G`, there exists a
group homomorphism `φ : G → Mˣ` such that `φ a ≠ 1`.  -/
CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity : ∀ (G : Type u_1) (M : Type u_2) [inst : CommGroup G] [Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] {a : G}, a ≠ 1 → ∃ φ, φ a ≠ 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_containsKey_insertListConst : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)}
  {k : α},
  Std.Internal.List.containsKey k (Std.Internal.List.insertListConst l toInsert) = true →
    (List.map Prod.fst toInsert).contains k = false → Std.Internal.List.containsKey k l = true
-- Init.Data.Array.BasicAux
Array.of_push_eq_push : ∀ {α : Type u_1} {a b : α} {as bs : Array α}, as.push a = bs.push b → as = bs ∧ a = b
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.minEntry?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.minEntry? = t₂.minEntry?
-- Mathlib.RingTheory.Ideal.Cotangent
/-- The lift of `f : A →ₐ[R] B` to `A ⧸ J ^ 2 →ₐ[R] B` with `J` being the kernel of `f`.  -/
AlgHom.kerSquareLift : {R : Type u} →
  [inst : CommRing R] →
    {A : Type u_1} →
      {B : Type u_2} →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (f : A →ₐ[R] B) → A ⧸ RingHom.ker f.toRingHom ^ 2 →ₐ[R] B
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.cosk_reflective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (n : ℕ)
  [inst_1 :
    ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F]
  [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F],
  CategoryTheory.IsIso (CategoryTheory.SimplicialObject.coskAdj n).counit
-- Mathlib.Topology.MetricSpace.Thickening
/-- The closed thickening of a compact set `E` is the union of the balls `Metric.closedBall x δ`
over `x ∈ E`.

See also `Metric.cthickening_eq_biUnion_closedBall`.  -/
IsCompact.cthickening_eq_biUnion_closedBall : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {δ : ℝ} {E : Set α},
  IsCompact E → 0 ≤ δ → Metric.cthickening δ E = ⋃ x ∈ E, Metric.closedBall x δ
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Nat.Partition.restricted.congr_simp : ∀ (n : ℕ) (p p_1 : ℕ → Prop),
  p = p_1 →
    ∀ {inst : DecidablePred p} [inst_1 : DecidablePred p_1],
      Nat.Partition.restricted n p = Nat.Partition.restricted n p_1
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.instSndScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  Ideal.absNorm (Ideal.span {hζ.toInteger - 1}) = p
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.Ordnode.ofAscListAux₁.match_1.splitter : {α : Type u_1} →
  (ys : List α) →
    (motive : Ordnode α × { l' // l'.length ≤ ys.length } → Sort u_2) →
      (x : Ordnode α × { l' // l'.length ≤ ys.length }) →
        ((r : Ordnode α) → (zs : List α) → (h' : zs.length ≤ ys.length) → motive (r, ⟨zs, h'⟩)) → motive x
-- Mathlib.Data.Set.Pairwise.Basic
pairwise_disjoint_mono : ∀ {α : Type u_1} {ι : Type u_4} {f g : ι → α} [inst : PartialOrder α] [inst_1 : OrderBot α],
  Pairwise (Function.onFun Disjoint f) → g ≤ f → Pairwise (Function.onFun Disjoint g)
-- Mathlib.RingTheory.Filtration
Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  [IsDomain R] [IsNoetherianRing R] [Module.IsTorsionFree R M] [Module.Finite R M], I ≠ ⊤ → ⨅ i, I ^ i • ⊤ = ⊥
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} [IsDomain R] {f v : Fin n → R},
  Function.Injective f → (∀ (j : Fin n), ∑ i, v i * f j ^ ↑i = 0) → v = 0
-- Mathlib.Topology.ContinuousOn
continuousOn_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {c : β},
  ContinuousOn (fun x => c) s
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.sum.of : ∀ {α : Type u} [inst : AddGroup α] {x : α}, (FreeGroup.of x).sum = x
-- Mathlib.Topology.Bornology.Hom
/-- Turn an element of a type `F` satisfying `LocallyBoundedMapClass F α β` into an actual
`LocallyBoundedMap`. This is declared as the default coercion from `F` to
`LocallyBoundedMap α β`.  -/
LocallyBoundedMapClass.toLocallyBoundedMap : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Bornology α] → [inst_2 : Bornology β] → [LocallyBoundedMapClass F α β] → F → LocallyBoundedMap α β
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.rightOp_full : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor Cᵒᵖ D} [F.Full], F.rightOp.Full
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tildeEquiv_unitIso : ∀ {R : CommRingCat}, AlgebraicGeometry.tildeEquiv.unitIso = AlgebraicGeometry.tilde.toTildeΓNatIso
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.instHasFirstPageComputationEIntProdIntCoreE₂Cohomological : CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological.HasFirstPageComputation
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_hom_naturality_assoc : ∀ {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}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c₁ c₂ c₃ c₄ : C} {d₁ d₂ : D} (f : c₁ ⟶ c₂)
  (g : c₃ ⟶ c₄) (h : d₁ ⟶ d₂) {Z : D}
  (h_1 :
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c₂
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c₄ d₂) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₂ c₄ d₂).hom h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₁ c₃ d₁).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom g h))
        h_1)
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.toAdicCompletion.eq_1 : ∀ (σ : Type u_3) (R : Type u_4) [inst : Finite σ] [inst_1 : CommRing R],
  MvPowerSeries.toAdicCompletion σ R =
    AdicCompletion.liftAlgHom (MvPolynomial.idealOfVars σ R) (MvPowerSeries.truncTotalAlgHom σ R) ⋯
-- Mathlib.Algebra.Order.Monovary
Monovary.mul_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : PartialOrder β] {f₁ f₂ : ι → α} {g : ι → β},
  0 ≤ f₁ → 0 ≤ f₂ → Monovary f₁ g → Monovary f₂ g → Monovary (f₁ * f₂) g
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.comap_id : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (C : ConvexCone R M), ConvexCone.comap LinearMap.id C = C
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.of_prim : ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ}, Primrec f → Nat.Primrec' f
-- Mathlib.CategoryTheory.Presentable.Type
/-- Any type `X` is the (filtered) colimit of its subsets of cardinality `< κ`
when `κ` is an infinite cardinal. (This colimit is `κ`-filtered when `κ` is
a regular cardinal.)  -/
HasCardinalLT.Set.isColimitCocone : (X : Type u) → (κ : Cardinal.{u}) → Cardinal.aleph0 ≤ κ → CategoryTheory.Limits.IsColimit (HasCardinalLT.Set.cocone X κ)
-- Lean.Meta.TryThis
/-- Style hooks for `Suggestion`s. See `SuggestionStyle.error`, `.warning`, `.success`, `.value`,
and other definitions here for style presets. This is an arbitrary `Json` object, with the following
interesting fields:
* `title`: the hover text in the suggestion link
* `className`: the CSS classes applied to the link
* `style`: A `Json` object with additional inline CSS styles such as `color` or `textDecoration`.
 -/
Lean.Meta.Tactic.TryThis.SuggestionStyle : Type
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.id.eq_1 : ∀ (M : Type u_10) [inst : AddZero M], AddMonoidHom.id M = { toFun := fun x => x, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- If `A` has doubling `K` strictly less than `φ`, then `A * A⁻¹` is covered by
at most a constant number of cosets of a finite subgroup of `G`.  -/
Finset.doubling_lt_golden_ratio : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A : Finset G},
  1 < K →
    K < Real.goldenRatio →
      ↑(A⁻¹ * A).card ≤ K * ↑A.card →
        ↑(A * A⁻¹).card ≤ K * ↑A.card →
          ∃ H x Z, ↑Z.card ≤ (2 - K) * K / ((Real.goldenRatio - K) * (K - Real.goldenConj)) ∧ ↑H * ↑Z = ↑A * ↑A⁻¹
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_right_le_mk_mul_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk b ≤ MulArchimedeanClass.mk (a * b) ↔ MulArchimedeanClass.mk b ≤ MulArchimedeanClass.mk a
-- Mathlib.Tactic.Bound.Attribute
/-- Map the arguments of an inequality expression to a score  -/
Mathlib.Tactic.Bound.ineqPriority : {u : Lean.Level} → {α : Q(Type u)} → Q(«$α») → Q(«$α») → Lean.MetaM ℕ
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_memLp : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {p : ENNReal},
  p ≠ 0 →
    p ≠ ⊤ → ∀ (f : MeasureTheory.SimpleFunc α E), MeasureTheory.MemLp (⇑f) p μ → ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
-- Mathlib.Analysis.Complex.IntegerCompl
Complex.integerComplement_pow_two_ne_pow_two : ∀ {x : ℂ}, x ∈ Complex.integerComplement → ∀ (n : ℤ), x ^ 2 ≠ ↑n ^ 2
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_add_eq_sum_add_of_exists : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {f : α →₀ M} {g : α → M → N}
  {n₁ n₂ : N}, ∀ a ∈ f.support, g a (f a) + n₁ = g a (f a) + n₂ → f.sum g + n₁ = f.sum g + n₂
-- Init.Data.SInt.Lemmas
Int8.add_left_inj : ∀ {a b : Int8} (c : Int8), a + c = b + c ↔ a = b
-- Mathlib.Order.Max
/-- **Alias** of the reverse direction of `isMin_ofDual_iff`. -/
IsMax.ofDual : ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMax a → IsMin (OrderDual.ofDual a)
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop.match_3.eq_2 : ∀ {α : Type u_1} (γ : Type u_1) (Pl : α → γ → ForInStep γ → Prop) (next : α) (acc : γ)
  (motive : Subtype (Pl next acc) → Sort u_2) (acc' : γ) (property : Pl next acc (ForInStep.done acc'))
  (h_1 : (acc' : γ) → (h' : Pl next acc (ForInStep.yield acc')) → motive ⟨ForInStep.yield acc', h'⟩)
  (h_2 : (acc' : γ) → (property : Pl next acc (ForInStep.done acc')) → motive ⟨ForInStep.done acc', property⟩),
  (match ⟨ForInStep.done acc', property⟩ with
    | ⟨ForInStep.yield acc', h'⟩ => h_1 acc' h'
    | ⟨ForInStep.done acc', property⟩ => h_2 acc' property) =
    h_2 acc' property
-- Init.Grind.Module.Basic
Lean.Grind.IntModule.zsmul_zero : ∀ {M : Type u} [inst : Lean.Grind.IntModule M] (n : ℤ), n • 0 = 0
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Under.mono_right_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.Limits.HasPullbacks C]
  {f g : CategoryTheory.Under X} (h : f ⟶ g) [CategoryTheory.Mono h],
  CategoryTheory.Mono (CategoryTheory.Under.Hom.right h)
-- Mathlib.MeasureTheory.Integral.IntervalAverage
/-- If `f : ℝ → ℝ` is continuous on `uIcc a b`, the interval has finite and nonzero `μ`-measure,
and `μ` has value zero on singletons, then `∃ c ∈ uIoo a b, f c = ⨍ x in Ι a b, f x ∂μ`.  -/
exists_eq_interval_average_of_nullSingletonClass : ∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ],
  ContinuousOn f (Set.uIcc a b) →
    μ (Set.uIoc a b) ≠ ⊤ → μ (Set.uIoc a b) ≠ 0 → ∃ c ∈ Set.uIoo a b, f c = ⨍ (x : ℝ) in Set.uIoc a b, f x ∂μ
-- Mathlib.Algebra.Group.Fin.Basic
Fin.addCommMonoid : (n : ℕ) → [NeZero n] → AddCommMonoid (Fin n)
-- Mathlib.GroupTheory.SpecificGroups.Alternating
/-- Shows that any non-identity element of $A_5$ whose cycle decomposition consists only of swaps
is conjugate to $(04)(13)$. This is used to show that the normal closure of such a permutation
in $A_5$ is $A_5$.  -/
alternatingGroup.isConj_swap_mul_swap_of_cycleType_two : ∀ {g : Equiv.Perm (Fin 5)},
  g ∈ alternatingGroup (Fin 5) → g ≠ 1 → (∀ n ∈ g.cycleType, n = 2) → IsConj (Equiv.swap 0 4 * Equiv.swap 1 3) g
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.State.mk : Array Bool → Array ℕ → ℕ → Bool → Lean.Util.ParamMinimizer.State✝
-- Mathlib.Algebra.Homology.Single
CochainComplex.single₀ObjXSelf : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] (X : V),
  HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 X =
    CategoryTheory.Iso.refl (((HomologicalComplex.single V (ComplexShape.up ℕ) 0).obj X).X 0)
-- Mathlib.Algebra.Lie.Basis.Basic
/-- As shown in `LieAlgebra.Basis.coroot_eq_h'` this is a coroot.  -/
LieAlgebra.Basis.h' : {ι : Type u_1} →
  {R : Type u_2} →
    {L : Type u_3} →
      [inst : Finite ι] →
        [inst_1 : CommRing R] →
          [inst_2 : LieRing L] → [inst_3 : LieAlgebra R L] → {H : LieSubalgebra R L} → LieAlgebra.Basis ι H → ι → ↥H
-- Init.Control.State
StateT.instMonad : {σ : Type u} → {m : Type u → Type v} → [Monad m] → Monad (StateT σ m)
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_nonneg : ∀ {K : Type u_1} [inst : RCLike K] (z : K), 0 ≤ RCLike.normSq z
-- Mathlib.Topology.MetricSpace.Pseudo.Real
Real.dist_le_of_mem_Icc_01 : ∀ {x y : ℝ}, x ∈ Set.Icc 0 1 → y ∈ Set.Icc 0 1 → dist x y ≤ 1
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceBackward_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X)
  {X_1 Y : CategoryTheory.Over f.left} (α : X_1 ⟶ Y),
  f.iteratedSliceBackward.map α =
    CategoryTheory.Over.homMk (CategoryTheory.Over.homMk (CategoryTheory.Over.Hom.left α) ⋯) ⋯
-- Mathlib.Algebra.Group.Units.Basic
Units.mul_inv_eq_one : ∀ {α : Type u} [inst : Monoid α] {u : αˣ} {a : α}, a * ↑u⁻¹ = 1 ↔ a = ↑u
-- Mathlib.Data.Nat.Squarefree
Nat.sq_mul_squarefree_of_pos : ∀ {n : ℕ}, 0 < n → ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
/-- Assume that `m ∣ n`, then the image of `ℚ(ζₘ) ⊆ ℚ(ζₙ)` by `intermediateFieldEquivSubgroupChar` is
the set of characters whose conductor divides `m`.
 -/
IsCyclotomicExtension.Rat.mem_intermediateFieldEquivSubgroupChar_iff_conductor_dvd : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [inst_3 : CommRing R]
  [inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [inst_5 : IsAbelianGalois ℚ K]
  (F : IntermediateField ℚ K) {m : ℕ} [NeZero m] [IsGalois ℚ ↥F] [IsCyclotomicExtension {m} ℚ ↥F],
  m ∣ n →
    ∀ (χ : DirichletCharacter R n),
      χ ∈ (IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar n K R) F ↔ χ.conductor ∣ m
-- Lean.Meta.Tactic.Grind.MatchCond
/-- Given a `match`-expression condition `e` that is known to be equal to `True`,
try to close the goal by proving `False`. We use the following to example to illustrate
the purpose of this function.
```
def f : List Nat → List Nat → Nat
  | _, 1 :: _ :: _ => 1
  | _, _ :: _ => 2
  | _, _  => 0

example : z = a :: as → y = z → f x y > 0 := by
  grind [f.eq_def]
```
After `grind` unfolds `f`, it case splits on the `match`-expression producing
three subgoals. The first two are easily closed by it. In the third one,
we have the following two `match`-expression conditions stating that we
are **not** in the first and second cases.
```
Lean.Grind.MatchCond (∀ (head : Nat) (tail : List Nat), x✝² = 1 :: head :: tail → False)
Lean.Grind.MatchCond (∀ (head : Nat) (tail : List Nat), x✝² = head :: tail → False)
```
Moreover, we have the following equivalence class.
```
{z, y, x✝², a :: as}
```
Thus, we can close the goal by using the second `match`-expression condition,
we just have to instantiate `head` and `tail` with `a` and `as` respectively,
and use the fact that `x✝²` is equal to `a :: as`.
 -/
Lean.Meta.Grind.tryToProveFalse : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- All n-simplices among cospherical points in n-space have the same
circumsphere.  -/
EuclideanGeometry.exists_circumsphere_eq_of_cospherical : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V],
  Module.finrank ℝ V = n →
    EuclideanGeometry.Cospherical ps →
      ∃ c, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.instMonadRingLinearM : Lean.Meta.Grind.Arith.CommRing.MonadRing Lean.Meta.Grind.Arith.Linear.LinearM
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
/-- Given a functor `C ⥤ D`, we obtain a morphism `nerve C ⟶ nerve D` of simplicial sets.  -/
CategoryTheory.nerveMap : {C D : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Category.{v, u} D] →
      CategoryTheory.Functor C D → (CategoryTheory.nerve C ⟶ CategoryTheory.nerve D)
-- Mathlib.Algebra.Homology.ShortComplex.Ab
/-- In a short exact sequence of abelian groups, the middle group is finite iff the first and last
are.  -/
CategoryTheory.ShortComplex.ShortExact.ab_finite_iff : ∀ {S : CategoryTheory.ShortComplex Ab}, S.ShortExact → (Finite ↑S.X₂ ↔ Finite ↑S.X₁ ∧ Finite ↑S.X₃)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_sub : ∀ {x : ℝ}, 0 < x → ∀ (y z : ℝ), x ^ (y - z) = x ^ y / x ^ z
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.map_id' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}, MeasureTheory.Measure.map (fun x => x) μ = μ
-- Lean.Parser.Tactic
Lean.Parser.Tactic.match.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Lean.LocalContext
/-- Return the result of `f` on the first local declaration on which `f` succeeds.  -/
Lean.LocalContext.firstDeclM : {m : Type u → Type v} → [AlternativeMonad m] → {β : Type u} → Lean.LocalContext → (Lean.LocalDecl → m β) → m β