mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The generic case of the first cosimplicial identity  -/
CategoryTheory.CosimplicialObject.δ_comp_δ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i j : Fin (n + 2)},
  i ≤ j →
    ∀ {Z : C} (h : X.obj { len := n + 1 + 1 } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (X.δ j.succ) h) =
        CategoryTheory.CategoryStruct.comp (X.δ j) (CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) h)
-- Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits
CategoryTheory.Adjunction.preservesColimitsOfShape_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {E : Type u₃}
  [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (H : CategoryTheory.Functor D E) (J : Type u)
  [inst_3 : CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasColimitsOfShape J C] [G.Full] [G.Faithful],
  CategoryTheory.Limits.PreservesColimitsOfShape J H ↔ CategoryTheory.Limits.PreservesColimitsOfShape J (F.comp H)
-- Mathlib.Order.WellFounded
Function.isMinimalFor_argmin : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) [inst : LinearOrder β] [inst_1 : WellFoundedLT β] [inst_2 : Nonempty α],
  MinimalFor (fun x => True) f (Function.argmin f)
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.row.eq_1 : ∀ (μ : YoungDiagram) (i : ℕ), μ.row i = {c ∈ μ.cells | c.1 = i}
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_op_subgroup : ∀ {G : Type u_1} [inst : Group G] (s : Subgroup G), MulAction.stabilizer Gᵐᵒᵖ ↑s = s.op
-- Mathlib.Analysis.Analytic.Composition
/-- The `0`-th coefficient of `q.comp p` is `q 0`. When `p` goes from `E` to `E`, this can be
expressed as a direct equality  -/
FormalMultilinearSeries.comp_coeff_zero'' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup E] [inst_8 : ContinuousConstSMul 𝕜 E] [inst_9 : IsTopologicalAddGroup F]
  [inst_10 : ContinuousConstSMul 𝕜 F] (q : FormalMultilinearSeries 𝕜 E F) (p : FormalMultilinearSeries 𝕜 E E),
  q.comp p 0 = q 0
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.instMonoICycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i],
  CategoryTheory.Mono (K.iCycles i)
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.const_mul : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α} {f : α → M}
  [MeasurableMul M], Measurable f → ∀ (c : M), Measurable fun x => c * f x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The discriminant `Δ'` of an elliptic curve over `R`, which is given as a unit in `R`.
Note that to prove two equal elliptic curves have the same `Δ'`, you need to use `simp_rw`,
as `rw` cannot transfer instance `WeierstrassCurve.IsElliptic` automatically.  -/
WeierstrassCurve.Δ' : {R : Type u} → [inst : CommRing R] → (W : WeierstrassCurve R) → [W.IsElliptic] → Rˣ
-- Init.System.IO
/-- Creates a temporary file in the most secure manner possible, returning both a `Handle` to the
already-opened file and its path.

There are no race conditions in the file’s creation. The file is readable and writable only by the
creating user ID. Additionally on UNIX style platforms the file is executable by nobody.

It is the caller's job to remove the file after use. Use `withTempFile` to ensure that the temporary
file is removed.
 -/
IO.FS.createTempFile : IO (IO.FS.Handle × System.FilePath)
-- Lean.Parser.Command
Lean.Parser.Command.openSimple : Lean.Parser.Parser
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The tangent of an angle in a right-angled triangle as a ratio of sides.  -/
EuclideanGeometry.tan_angle_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 → Real.tan (EuclideanGeometry.angle p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.copy_e : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.MonoFactorisation f) (m : F.I ⟶ Y) (e : X ⟶ F.I)
  (hm : autoParam (m = F.m) CategoryTheory.Limits.MonoFactorisation.copy._auto_1)
  (he : autoParam (e = F.e) CategoryTheory.Limits.MonoFactorisation.copy._auto_3), (F.copy m e hm he).e = e
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.liftOfLE_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M₁ : Type u_7}
  {M₂ : Type u_6} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₁] [inst_6 : Module R M₂]
  (S₁ S₂ : Submonoid R) (h : S₁ ≤ S₂) (f₁ : M →ₗ[R] M₁) (f₂ : M →ₗ[R] M₂) [inst_7 : IsLocalizedModule S₁ f₁]
  [inst_8 : IsLocalizedModule S₂ f₂] (x : M), (IsLocalizedModule.liftOfLE S₁ S₂ h f₁ f₂) (f₁ x) = f₂ x
-- Mathlib.Data.Tree.Basic
BinaryTree.numNodes.eq_1 : ∀ {α : Type u}, BinaryTree.nil.numNodes = 0
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.ofFun_one : ∀ {α : Type u_1} {β : Type u_2} [inst : One β], UniformFun.ofFun 1 = 1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∪ t₂).get? k = (t₂.get? k).or (t₁.get? k)
-- Mathlib.LinearAlgebra.Ray
RayVector.ext_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Zero M] {x y : RayVector R M},
  x = y ↔ ↑((RayVector.equiv R M) x) = ↑((RayVector.equiv R M) y)
-- Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
HasFDerivAtFilter.of_comp_of_isEmbedding : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {g' : E →L[𝕜] F}
  {f' : F →L[𝕜] G} {lE : Filter (E × E)} {lF : Filter (F × F)},
  Filter.Tendsto (Prod.map g g) lE lF →
    HasFDerivAtFilter f f' lF →
      Topology.IsEmbedding ⇑f' →
        HasFDerivAtFilter h (f' ∘SL g') lE → Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h → HasFDerivAtFilter g g' lE
-- Mathlib.CategoryTheory.Sigma.Basic
/-- This shows that when `desc F` is restricted to just the subcategory `C i`, `desc F` agrees with
`F i`.
 -/
CategoryTheory.Sigma.inclDesc : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (F : (i : I) → CategoryTheory.Functor (C i) D) →
            (i : I) → (CategoryTheory.Sigma.incl i).comp (CategoryTheory.Sigma.desc F) ≅ F i
-- Mathlib.Tactic.Ring.Common
/-- Cast `ExSumNat` to `ExSum btℕ sℕ`.  -/
Mathlib.Tactic.Ring.Common.ExSumNat.toExSum : (e : Q(ℕ)) →
  Mathlib.Tactic.Ring.Common.ExSumNat e →
    (e' : Q(ℕ)) × Mathlib.Tactic.Ring.Common.ExSum Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ e'
-- Mathlib.Order.Cover
CovBy.of_le_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a ⋖ c → a ≤ b → b < c → b ⋖ c
-- Mathlib.Algebra.Group.Even
Even.isSquare_pow : ∀ {α : Type u_2} [inst : Monoid α] {n : ℕ}, Even n → ∀ (a : α), IsSquare (a ^ n)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  (g : Y ⟶ Z) [AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] [AlgebraicGeometry.SheafedSpace.IsOpenImmersion g],
  AlgebraicGeometry.SheafedSpace.IsOpenImmersion (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalenceFunctor_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G)
  (g : CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G)),
  ((CategoryTheory.StructuredArrow.preEquivalenceFunctor F f).obj g).right = g.right.right
-- Std.Time.Format.Modifier
Std.Time.OffsetX.hourMinute.sizeOf_spec : sizeOf Std.Time.OffsetX.hourMinute = 1
-- Mathlib.Util.TermReduce
/-- `reduceProj% t` apply `Expr.reduceProjStruct?` to all subexpressions of `t`.  -/
Mathlib.Util.TermReduce.elabReduceProj : Lean.Elab.Term.TermElab
-- Mathlib.RingTheory.NormalClosure
Ring.instAlgebraNormalClosure : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : IsDomain R] →
          [inst_3 : IsDomain S] →
            [inst_4 : Algebra R S] → [inst_5 : Module.IsTorsionFree R S] → Algebra S (Ring.NormalClosure R S)
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsMinOn.hasLineDerivWithinAt_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E} {f' : ℝ},
  IsMinOn f s a → HasLineDerivWithinAt ℝ f f' s a b → (∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) → f' = 0
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Delaborates a rational number literal.
`@OfNat.ofNat _ n _ / @OfNat.ofNat _ m` ~> `n / m`
and `-@OfNat.ofNat _ n _ / @OfNat.ofNat _ m` ~> `-n / m`
 -/
Lean.PrettyPrinter.Delaborator.delabHDiv : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.instNeg : {R : Type u_2} → {M : Type u_3} → [Neg R] → Neg (Mathlib.Tactic.Module.NF R M)
-- Std.Sync.StreamMap
/-- Create an empty StreamMap
 -/
Std.StreamMap.empty : {β α : Type} → Std.StreamMap α β
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.baseChange_val : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_2)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] (P : Algebra.Generators R S ι) (x : ι),
  (Algebra.Generators.baseChange T P).val x = 1 ⊗ₜ[R] P.val x
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.length_toList_eq_count : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β}, it.toList.length = it.length
-- Mathlib.Data.Matrix.Basis
Matrix.mul_single_apply_same : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n]
  [inst_2 : Fintype m] [inst_3 : NonUnitalNonAssocSemiring α] (c : α) (i : m) (j : n) (a : l) (M : Matrix l m α),
  (M * Matrix.single i j c) a j = M a i * c
-- Mathlib.MeasureTheory.Group.Arithmetic
aemeasurable_const_smul_iff₀ : ∀ {G₀ : Type u_3} {β : Type u_5} {α : Type u_6} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace α] {f : α → β}
  {μ : MeasureTheory.Measure α} [inst_2 : GroupWithZero G₀] [inst_3 : MulAction G₀ β] [MeasurableConstSMul G₀ β]
  {c : G₀}, c ≠ 0 → (AEMeasurable (fun x => c • f x) μ ↔ AEMeasurable f μ)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.not_nonempty_empty : ¬∅.Nonempty
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.orOver_of_p : ∀ {i n : ℕ} {p : ℕ → Prop}, i < n → p i → Int.Internal.Linear.OrOver n p
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_succ : ∀ (o : Ordinal.{u_1}), Cardinal.beth (Order.succ o) = 2 ^ Cardinal.beth o
-- Mathlib.Analysis.Analytic.Composition
/-- Rewriting equality in the dependent type `Σ (a : Composition n), Composition a.length)` in
non-dependent terms with lists, requiring that the blocks coincide.  -/
Composition.sigma_composition_eq_iff : ∀ {n : ℕ} (i j : (a : Composition n) × Composition a.length),
  i = j ↔ i.fst.blocks = j.fst.blocks ∧ i.snd.blocks = j.snd.blocks
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.fwd : Lean.Meta.Grind.EMatchTheoremKind
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
dist_pi_le_iff : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)]
  {f g : (b : β) → X b} {r : ℝ}, 0 ≤ r → (dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Basic.0.Matrix.termε_ : Lean.ParserDescr
-- Mathlib.RingTheory.Idempotents
/-- A family `{ eᵢ }` of idempotent elements is orthogonal if `eᵢ * eⱼ = 0` for all `i ≠ j`.  -/
OrthogonalIdempotents : {R : Type u_1} → [Semiring R] → {I : Type u_3} → (I → R) → Prop
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
/-- If `R : InjectiveResolution X`, this is the cochain complex indexed by `ℤ`
obtained by extending by zero the cochain complex `R.cocomplex` indexed by `ℕ`.  -/
CategoryTheory.InjectiveResolution.cochainComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Preadditive C] → {X : C} → CategoryTheory.InjectiveResolution X → CochainComplex C ℤ
-- Lean.Attributes
Lean.registerParametricAttribute : {α : Type} → Lean.ParametricAttributeImpl α → IO (Lean.ParametricAttribute α)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_getElem?_eq_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t[a]?.isSome = t.contains a
-- Init.Data.SInt.Bitwise
Int64.or_comm : ∀ (a b : Int64), a ||| b = b ||| a
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- If `colim` of shape `J` into an abelian category `C` preserves monomorphisms, then `C` has exact
colimits of shape `J`.
 -/
CategoryTheory.hasExactColimitsOfShape_of_preservesMono : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (J : Type u')
  [inst_2 : CategoryTheory.Category.{v', u'} J] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  [CategoryTheory.Limits.colim.PreservesMonomorphisms], CategoryTheory.HasExactColimitsOfShape J C
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nsmul_subset_nsmul_left : ∀ {α : Type u_2} [inst : AddMonoid α] {s t : Set α} {n : ℕ}, s ⊆ t → n • s ⊆ n • t
-- Init.Data.Rat.Lemmas
Rat.neg_add_cancel : ∀ (a : ℚ), -a + a = 0
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.equivPresentedGroup_apply_of : ∀ {α : Type u_1} {β : Type u_2} (x : α) (rels : Set (FreeGroup α)) (e : α ≃ β),
  (PresentedGroup.equivPresentedGroup rels e) (PresentedGroup.of x) = PresentedGroup.of (e x)
-- Mathlib.Order.Disjoint
isCompl_toDual_iff : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {a b : α},
  IsCompl (OrderDual.toDual a) (OrderDual.toDual b) ↔ IsCompl a b
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.objEquiv_apply_fst' : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d) (i : Fin (d + 1)), (x.cast hd).simplex.1 i = (x.cast hd).simplex.1 i
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.oracle : ∀ {O : Set (ℕ →. ℕ)}, ∀ g ∈ O, Nat.RecursiveIn O g
-- Init.Data.String.Termination
String.Pos.ne_endPos_of_next?_eq_some : ∀ {s : String} {p q : s.Pos}, p.next? = some q → p ≠ s.endPos
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_alter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)},
  (m.alter k f).getKey? k' =
    if (k == k') = true then if (f (m.get? k)).isSome = true then some k else none else m.getKey? k'
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.isInitial_omega0 : Ordinal.omega0.IsInitial
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.mk'.eq_1 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (L R : Turing.ListBlank Γ),
  Turing.Tape.mk' L R = { head := R.head, left := L, right := R.tail }
-- Mathlib.GroupTheory.OrderOfElement
AddSubgroup.nsmul_relIndex_mem : ∀ {G : Type u_6} [inst : AddGroup G] (H : AddSubgroup G) [H.Normal] {K : AddSubgroup G} {g : G},
  g ∈ K → H.relIndex K • g ∈ H
-- Lean.Elab.App
/-- We annotate recursive applications with their `Syntax` node to make sure we can produce error messages with
correct position information at `WF` and `Structural`.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.annotateIfRec : Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Tactic.DeriveTraversable
/-- Prove the traversable laws and derive `LawfulTraversable`.  -/
Mathlib.Deriving.Traversable.deriveLawfulTraversable : Lean.MVarId → Lean.Elab.TermElabM Unit
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.toComposition_blocks : ∀ {n : ℕ} (c : CompositionAsSet n), c.toComposition.blocks = c.blocks
-- Mathlib.Data.ENat.Basic
ENat.lift_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).lift ⋯ = OfNat.ofNat n
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_div_mul_cancel : ∀ {a : Ordinal.{u_4}}, a ≠ 0 → ∀ (b c : Ordinal.{u_4}), a * b / (a * c) = b / c
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- `f : X → C(α, β)` is continuous if any only if it is continuous when reinterpreted as a
map `f : X → α →ᵤ[{K | IsCompact K}] β`.  -/
ContinuousMap.continuous_iff_continuous_uniformOnFun : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {X : Type u_1}
  [inst_2 : TopologicalSpace X] (f : X → C(α, β)),
  Continuous f ↔ Continuous fun x => (UniformOnFun.ofFun {K | IsCompact K}) ⇑(f x)
-- Init.Data.Rat.Basic
/-- The denominator is nonzero.  -/
Rat.den_nz : ∀ (self : ℚ), self.den ≠ 0
-- Std.Time.Internal.Bounded
/-- Returns the maximum between a number and the bounded.
 -/
Std.Time.Internal.Bounded.LE.max : {n m : ℤ} → Std.Time.Internal.Bounded.LE n m → (val : ℤ) → Std.Time.Internal.Bounded.LE (max n val) (max m val)
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.orthogonalProjection_affineSpan_singleton : ∀ {𝕜 : 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] (p₁ p₂ : P),
  ↑((EuclideanGeometry.orthogonalProjection (affineSpan 𝕜 {p₁})) p₂) = p₁
-- Init.Data.Option.Lemmas
Option.pfilter_le : ∀ {α : Type u_1} [inst : LE α], (∀ (x : α), x ≤ x) → ∀ {o : Option α} {p : (a : α) → o = some a → Bool}, o.pfilter p ≤ o
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.IsSymm.smul : ∀ {α : Type u_1} {n : Type u_3} {R : Type u_5} [inst : SMul R α] {A : Matrix n n α},
  A.IsSymm → ∀ (k : R), (k • A).IsSymm
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_univ_two : ∀ {M : Type u_2} [inst : AddCommMonoid M] (f : Fin 2 → M), ∑ i, f i = f 0 + f 1
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- Converse to the mean value inequality: if `f` is differentiable at `x₀` and `C`-lipschitz
then its derivative at `x₀` has norm bounded by `C`.  -/
HasFDerivAt.le_of_lipschitz : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x₀ : E}, HasFDerivAt f f' x₀ → ∀ {C : NNReal}, LipschitzWith C f → ‖f'‖ ≤ ↑C
-- Mathlib.RingTheory.Nakayama
Submodule.top_ne_set_smul_of_subset_jacobson_annihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial M]
  [Module.Finite R M] {s : Set R}, s ⊆ ↑(Module.annihilator R M).jacobson → ⊤ ≠ s • ⊤
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.instNoncompactSpace : ∀ {α : Type u_1} [inst : UniformSpace α] [NoncompactSpace α], NoncompactSpace (TopologicalSpace.Closeds α)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.instRegularOfIsAddHaarMeasureOfCompactSpace : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] [CompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ], μ.Regular
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  (Std.TreeSet.Raw.ofList l cmp).isEmpty = l.isEmpty
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.adj : ∀ {V : Type u_1} {G : SimpleGraph V} (self : G.Dart), G.Adj self.toProd.1 self.toProd.2
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono_attachCells_ι : ∀ {X Y : SSet} (i : X ⟶ Y) [inst : CategoryTheory.Mono i] (d : ℕ) (x : ¬IsMax d),
  ((SSet.relativeCellComplexOfMono i).attachCells d x).ι = SSet.relativeCellComplexOfMono.Cell i d
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- **Noether's third isomorphism theorem** for additive groups: `(A / N) / (M / N) ≃+ A / M`.  -/
QuotientAddGroup.quotientQuotientEquivQuotient : {G : Type u} →
  [inst : AddGroup G] →
    (N : AddSubgroup G) →
      [nN : N.Normal] →
        (M : AddSubgroup G) → [nM : M.Normal] → N ≤ M → (G ⧸ N) ⧸ AddSubgroup.map (QuotientAddGroup.mk' N) M ≃+ G ⧸ M
-- Aesop.Forward.State
Aesop.ClusterState.AddM.Context.mk.sizeOf_spec : ∀ (premiseMVars : Array Lean.MVarId) (premiseLMVars : Array Lean.LMVarId),
  sizeOf { premiseMVars := premiseMVars, premiseLMVars := premiseLMVars } =
    1 + sizeOf premiseMVars + sizeOf premiseLMVars
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The augmented Čech nerve of the map from `Fin 1 → G` to the terminal object in `Type u` has an
extra degeneracy.  -/
classifyingSpaceUniversalCover.extraDegeneracyAugmentedCechNerve : (G : Type u) →
  [Monoid G] → (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from G)).augmentedCechNerve.ExtraDegeneracy
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.nil.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf RBTree.RBNode.nil = 1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertMax!.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.insertMax! k v t =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf =>
      Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r' =>
      Std.DTreeMap.Internal.Impl.balanceR! k' v' l' (Std.DTreeMap.Internal.Impl.insertMax! k v r')
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instSMul.eq_1 : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α], Lex.instSMul = inst
-- Mathlib.Tactic.DefEqAbuse
/-- Within a synthesis trace, find failing `apply @Instance to Goal` nodes
and their `isDefEq` transition failures.
Once https://github.com/leanprover/lean4/pull/12699 is available, the `headerStr.contains "apply"`
check can be replaced with ``td.cls == `Meta.synthInstance.apply``.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Mathlib.Tactic.DefEqAbuse.findSynthAppFailures : Std.HashSet String → Std.HashSet String → Lean.MessageData → BaseIO (Array (Lean.MessageData × Array Lean.MessageData))