mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PowerSeries.Schroder
/-- The power series for large Schröder numbers  -/
PowerSeries.largeSchroderSeries : PowerSeries ℕ
-- Batteries.Data.List.Lemmas
List.countPBefore_length : ∀ {α : Type u_1} {p : α → Bool} {xs : List α}, List.countPBefore p xs xs.length = List.countP p xs
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.map_surjective : ∀ {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (α i)]
  [inst_1 : (i : ι) → AddCommMonoid (β i)] (f : (i : ι) → α i →+ β i),
  Function.Surjective ⇑(DirectSum.map f) ↔ ∀ (i : ι), Function.Surjective ⇑(f i)
-- Mathlib.Order.Bounds.Image
image2_upperBounds_upperBounds_subset : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → Set.image2 f (upperBounds s) (upperBounds t) ⊆ upperBounds (Set.image2 f s t)
-- Mathlib.Algebra.EuclideanDomain.Basic
/-- If `S` is a nontrivial commutative ring isomorphic to a Euclidean domain
`R` then it is also a Euclidean domain.  -/
RingEquiv.euclideanDomain : {R : Type u_1} → {S : Type u_2} → [inst : EuclideanDomain R] → [inst_1 : CommRing S] → S ≃+* R → EuclideanDomain S
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A set `s` is called *complete*, if any Cauchy filter `f` such that `s ∈ f`
has a limit in `s` (formally, it satisfies `f ≤ 𝓝 x` for some `x ∈ s`).  -/
IsComplete : {α : Type u} → [uniformSpace : UniformSpace α] → Set α → Prop
-- Mathlib.Data.Num.Basic
/-- Subtraction of two `PosNum`s, producing a `ZNum`.  -/
PosNum.sub' : PosNum → PosNum → ZNum
-- Mathlib.RingTheory.FiniteLength
LinearEquiv.isFiniteLength : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : M ≃ₗ[R] N), IsFiniteLength R M → IsFiniteLength R N
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.nonempty_of_mem : ∀ {α : Type u} {f : Ultrafilter α} {s : Set α}, s ∈ f → s.Nonempty
-- Mathlib.RingTheory.PowerBasis
/-- `pb.minpolyGen` is the minimal polynomial for `pb.gen`.  -/
PowerBasis.minpolyGen : {S : Type u_2} →
  [inst : Ring S] → {A : Type u_4} → [inst_1 : CommRing A] → [inst_2 : Algebra A S] → PowerBasis A S → Polynomial A
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_mul_X_eq_monomial : ∀ {R : Type u_1} [inst : Semiring R] {a : R} [inst_1 : MulSemiringAction (Multiplicative ℕ) R],
  SkewPolynomial.C a * SkewPolynomial.X = (SkewPolynomial.monomial 1) a
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- An `α`-indexed cochain complex is a `HomologicalComplex`
in which `d i j ≠ 0` only if `i + 1 = j`.
 -/
CochainComplex : (V : Type u) →
  [inst : CategoryTheory.Category.{v, u} V] →
    [CategoryTheory.Limits.HasZeroMorphisms V] →
      (α : Type u_2) → [AddRightCancelSemigroup α] → [One α] → Type (max (max u_2 u) v)
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- `s` is the morphism witnessing symmetry  -/
CategoryTheory.SymmetricRelation.s : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} → {p₁ p₂ : R ⟶ X} → CategoryTheory.SymmetricRelation p₁ p₂ → (R ⟶ R)
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.Q_f_idem_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q n : ℕ) {Z : C}
  (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n)
      (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n) h) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n) h
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.coe_singletonOneHom : ∀ {α : Type u_2} [inst : One α], ⇑Set.singletonOneHom = singleton
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.variableChange_a₄ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R),
  (C • W).a₄ =
    ↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.incMatrix_of_mem_incidenceSet : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : MulZeroOneClass R] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] {a : α} {e : Sym2 α}, e ∈ G.incidenceSet a → SimpleGraph.incMatrix R G a e = 1
-- Batteries.Tactic.ShowUnused
_private.Batteries.Tactic.ShowUnused.0.Batteries.Tactic.ShowUnused.visit : Lean.Environment → Lean.Name → StateM Lean.NameSet Unit
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.inv.instSFinite : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Inv G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ],
  MeasureTheory.SFinite μ.inv
-- Init.Data.Array.InsertIdx
Array.insertIdx_zero : ∀ {α : Type u} {xs : Array α} {x : α}, xs.insertIdx 0 x ⋯ = #[x] ++ xs
-- Mathlib.Probability.Martingale.OptionalSampling
MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const : ∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : TopologicalSpace ι]
  [OrderTopology ι] [FirstCountableTopology ι] {ℱ : MeasureTheory.Filtration ι m}
  [MeasureTheory.SigmaFiniteFiltration μ ℱ] {τ : Ω → WithTop ι} {f : ι → Ω → E} {n : ι},
  MeasureTheory.Martingale f ℱ μ →
    ∀ (hτ : MeasureTheory.IsStoppingTime ℱ τ) (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) [MeasureTheory.SigmaFinite (μ.trim ⋯)]
      (i : ι), μ[f n | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = ↑i}] f i
-- Mathlib.Algebra.Jordan.Basic
IsJordan.rmul_comm_rmul_rmul : ∀ {A : Type u_1} {inst : Mul A} [self : IsJordan A] (a b : A), b * a * (a * a) = b * (a * a) * a
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.coeff_mul_single_add : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a b : Γ},
  (x * (HahnSeries.single b) r).coeff (a + b) = x.coeff a * r
-- Mathlib.CategoryTheory.Bicategory.Free
/-- Relations between 2-morphisms in the free bicategory.  -/
CategoryTheory.FreeBicategory.Rel : {B : Type u} →
  [inst : Quiver B] →
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} → CategoryTheory.FreeBicategory.Hom₂ f g → CategoryTheory.FreeBicategory.Hom₂ f g → Prop
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.mem_mk : ∀ {α : Type u_1} [inst : LE α] {s : Set α} (hs : IsLowerSet s) {a : α}, a ∈ { carrier := s, lower' := hs } ↔ a ∈ s
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.homRestrict.f_eq : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (ψ : K ⟶ L.extend e) {i : ι} {i' : ι'} (h : e.f i = i'),
  ComplexShape.Embedding.homRestrict.f ψ i =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e h).hom
      (CategoryTheory.CategoryStruct.comp (ψ.f i') (L.extendXIso e h).hom)
-- Mathlib.Algebra.Ring.Shrink
Shrink.instIsDomain : ∀ {α : Type u_1} [inst : Small.{v, u_1} α] [inst_1 : Semiring α] [IsDomain α], IsDomain (Shrink.{v, u_1} α)
-- Mathlib.Logic.IsEmpty.Basic
nonempty_fun : ∀ {α : Sort u_1} {β : Sort u_2}, Nonempty (α → β) ↔ IsEmpty α ∨ Nonempty β
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.length_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (SimpleGraph.Walk.cons h p).length = p.length + 1
-- Mathlib.FieldTheory.Galois.Infinite
InfiniteGalois.fixingSubgroup_isClosed : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (L : IntermediateField k K)
  [IsGalois k K], IsClosed ↑L.fixingSubgroup
-- Mathlib.Geometry.Euclidean.Projection
/-- The orthogonal projection of a point `p` onto the hyperplane spanned by the simplex's points.  -/
Affine.Simplex.orthogonalProjectionSpan : {𝕜 : 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] →
                {n : ℕ} → (s : Affine.Simplex 𝕜 P n) → P →ᴬ[𝕜] ↥(affineSpan 𝕜 (Set.range s.points))
-- Init.Data.List.Basic
List.erase_cons : ∀ {α : Type u} [inst : BEq α] {a b : α} {l : List α}, (b :: l).erase a = if (b == a) = true then l else b :: l.erase a
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_eq_zero : ∀ {K : Type u_1} [inst : RCLike K] {x : ℝ}, ↑x = 0 ↔ x = 0
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Precomp.map_succ_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left) (i j : ℕ) (hi : i + 1 < n + 1 + 1) (hj : j + 1 < n + 1 + 1) (hij : i + 1 ≤ j + 1),
  CategoryTheory.ComposableArrows.Precomp.map F f ⟨i + 1, hi⟩ ⟨j + 1, hj⟩ hij = F.map' i j ⋯ ⋯
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertOffset : Std.Time.TimeZone.Offset → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.subset_add_left : ∀ {α : Type u_2} [inst : AddZeroClass α] (s : Set α) {t : Set α}, 0 ∈ t → s ⊆ s + t
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- if `f` is integrable, then `fun x ↦ f x + g x` is integrable iff `g` is.
See `integrable_add_iff_integrable_right` for the same statement with `f + g` instead
of `fun x ↦ f x + g x`.  -/
MeasureTheory.integrable_add_iff_integrable_right' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f g : α → β},
  MeasureTheory.Integrable f μ → (MeasureTheory.Integrable (fun x => f x + g x) μ ↔ MeasureTheory.Integrable g μ)
-- Mathlib.Algebra.Group.Action.Hom
/-- A multiplicative action of `M` on `α` and a monoid homomorphism `N → M` induce
a multiplicative action of `N` on `α`.

See note [reducible non-instances].  -/
MulAction.compHom : {M : Type u_1} →
  {N : Type u_2} → (α : Type u_3) → [inst : Monoid M] → [MulAction M α] → [inst_2 : Monoid N] → (N →* M) → MulAction N α
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cotrident.ofπ_ι_app : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {P : C} (π : Y ⟶ P)
  (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π)
  (X_1 : CategoryTheory.Limits.WalkingParallelFamily J),
  (CategoryTheory.Limits.Cotrident.ofπ π w).ι.app X_1 =
    CategoryTheory.Limits.WalkingParallelFamily.casesOn X_1
      (CategoryTheory.CategoryStruct.comp (f (Classical.arbitrary J)) π) π
-- Lean.Meta.Sym.Apply
/-- Creates a `BackwardRule` from a declaration name.

The `num?` parameter optionally limits how many arguments are included in the pattern
(useful for partially applying theorems).
 -/
Lean.Meta.Sym.mkBackwardRuleFromDecl : Lean.Name → optParam (Option ℕ) none → Lean.MetaM Lean.Meta.Sym.BackwardRule
-- Mathlib.Order.Disjoint
IsCompl.disjoint_left_iff : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y z : α}, IsCompl y z → (Disjoint x y ↔ x ≤ z)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_toSubsemigroup : ∀ {M : Type u_2} [inst : AddZeroClass M] (H : AddSubmonoid M), H.op.toAddSubsemigroup = H.op
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.toCostructuredArrow_comp_proj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F),
  c.toCostructuredArrow.comp (CategoryTheory.CostructuredArrow.proj F c.pt) = CategoryTheory.Functor.id J
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instCompleteSpace : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] [CompleteSpace A],
  CompleteSpace (DoubleCentralizer 𝕜 A)
-- Init.Conv
/-- `next => tac` focuses on the next goal and solves it using `tac`, or else fails.
`next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
inaccessible names to the given names.
 -/
Lean.Parser.Tactic.Conv.«convNext__=>_» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_div_iff_mul_le' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LE α] [MulLeftMono α] {a b c : α}, b ≤ c / a ↔ a * b ≤ c
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.id.eq_1 : ∀ {α : Type u_1} {mα : MeasurableSpace α}, ProbabilityTheory.Kernel.id = ProbabilityTheory.Kernel.deterministic id ⋯
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.toSubalgebra_le_toSubalgebra : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {S S' : IntermediateField K L}, S.toSubalgebra ≤ S'.toSubalgebra ↔ S ≤ S'
-- Mathlib.Order.DirSupClosed
DirSupClosedOn.union : ∀ {α : Type u_1} {s t : Set α} {D : Set (Set α)} [inst : Preorder α],
  IsLowerSet D → DirSupClosedOn D s → DirSupClosedOn D t → DirSupClosedOn D (s ∪ t)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.toMultilinearAddHom_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : ContinuousAdd N] (f : M [⋀^ι]→L[R] N),
  ContinuousAlternatingMap.toMultilinearAddHom f = f.toContinuousMultilinearMap
-- Mathlib.Topology.Sets.CompactOpenCovered
IsCompactOpenCovered.image : ∀ {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [inst : (i : ι) → TopologicalSpace (X i)]
  {i : ι} (V : TopologicalSpace.Opens (X i)), IsCompact ↑V → IsCompactOpenCovered f (f i '' ↑V)
-- Lean.DocString.Types
Lean.Doc.Part.brecOn.eq : ∀ {i : Type u} {b : Type v} {p : Type w} {motive_1 : Lean.Doc.Part i b p → Sort u_1}
  {motive_2 : Array (Lean.Doc.Part i b p) → Sort u_1} {motive_3 : List (Lean.Doc.Part i b p) → Sort u_1}
  (t : Lean.Doc.Part i b p) (F_1 : (t : Lean.Doc.Part i b p) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.Part i b p)) → Lean.Doc.Part.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.Doc.Part i b p)) → Lean.Doc.Part.below_2 t → motive_3 t),
  t.brecOn F_1 F_2 F_3 = F_1 t (Lean.Doc.Part.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.RingTheory.Etale.Kaehler
Algebra.H1Cotangent.isLocalizedModule : ∀ (R : Type u_1) {S : Type u_2} (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] (M : Submonoid S)
  [IsLocalization M T], IsLocalizedModule M (Algebra.H1Cotangent.map R R S T)
-- Mathlib.Algebra.Ring.Subring.IntPolynomial
Polynomial.int_leadingCoeff_eq : ∀ {K : Type u_1} [inst : Field K] (R : Subring K) (P : Polynomial K) (hP : ∀ (n : ℕ), P.coeff n ∈ R),
  ↑(Polynomial.int R P hP).leadingCoeff = P.leadingCoeff
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.toOuterMeasure_ofFinset_apply : ∀ {α : Type u_1} {f : α → ENNReal} {s : Finset α} (h : ∑ a ∈ s, f a = 1) (h' : ∀ a ∉ s, f a = 0) (t : Set α),
  (PMF.ofFinset f s h h').toOuterMeasure t = ∑' (x : α), t.indicator f x
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalRingHom.closure_preimage_le : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R →ₙ+* S)
  (s : Set S), NonUnitalSubring.closure (⇑f ⁻¹' s) ≤ NonUnitalSubring.comap f (NonUnitalSubring.closure s)
-- Mathlib.Data.Nat.Init
Nat.two_lt_of_ne : ∀ {n : ℕ}, n ≠ 0 → n ≠ 1 → n ≠ 2 → 2 < n
-- Init.Data.UInt.Bitwise
UInt16.ofFin_shiftLeft_mod : ∀ (a b : Fin UInt16.size), UInt16.ofFin (a <<< (b % 16)) = UInt16.ofFin a <<< UInt16.ofFin b
-- Mathlib.Order.Filter.Defs
Filter.neBot_iff : ∀ {α : Type u_1} {f : Filter α}, f.NeBot ↔ f ≠ ⊥
-- Mathlib.SetTheory.Lists
Lists'.Subset.nil : ∀ {α : Type u_1} {l : Lists' α true}, Lists'.nil.Subset l
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- The trailing coefficient of the inverse function is the inverse of the trailing coefficient.
 -/
meromorphicTrailingCoeffAt_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {f : 𝕜 → 𝕜},
  meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.card_nsmul_le_sum : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] [AddLeftMono N] (s : Finset ι)
  (f : ι → N) (n : N), (∀ x ∈ s, n ≤ f x) → s.card • n ≤ s.sum f
-- Mathlib.AlgebraicGeometry.Artinian
/-- A commutative ring `R` is Artinian if and only if `Spec R` is an Artinian scheme  -/
AlgebraicGeometry.Scheme.isArtinianScheme_Spec : ∀ {R : CommRingCat}, AlgebraicGeometry.IsArtinianScheme (AlgebraicGeometry.Spec R) ↔ IsArtinianRing ↑R
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.cancel_natIso_inv_right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) {W X X' : D} {Y : C} (f : W ⟶ X) (g : X ⟶ G.obj Y) (f' : W ⟶ X')
  (g' : X' ⟶ G.obj Y),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (α.inv.app Y)) =
      CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (α.inv.app Y)) ↔
    CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
-- Mathlib.CategoryTheory.Limits.EpiMono
CategoryTheory.mono_iff_fst_eq_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : X ⟶ Y}
  {c : CategoryTheory.Limits.PullbackCone f f} (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.Mono f ↔ c.fst = c.snd
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.smul_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {m n : ℕ},
  m ≤ n →
    ∀ (r : AdicCompletion.AdicCauchySequence I R) (x : AdicCompletion.AdicCauchySequence I M),
      ↑r n • Submodule.Quotient.mk (↑x n) = ↑r m • Submodule.Quotient.mk (↑x m)
-- Mathlib.Algebra.Group.End
/-- If `M` is a type with addition, then additive automorphisms of `M` have the
structure of a group.

We give `AddAut M` the structure of an additive group rather than a multiplicative group to help
with `to_additive` translation. Without this, any proof in group theory making use of the
conjugation action `G →* MulAut G` would be impossible to `to_additive`-ize because a correct
additivization would require inserting `Additive` around `AddAut G` and dealing with these extra
`Additive`s in the proof, but `to_additive` is unable to do this automatically.  -/
AddAut.instAddGroup : (M : Type u_2) → [inst : Add M] → AddGroup (AddAut M)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_equivProd_symm_apply : ∀ {R : Type u_1} (c₁ c₂ c₃ : R) (a : R × R × R × R), ((QuaternionAlgebra.equivProd c₁ c₂ c₃).symm a).re = a.1
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- **Alias** of the reverse direction of `threeGPFree_image`.

---

Geometric progressions of length three are unchanged under `2`-Freiman isomorphisms.  -/
ThreeGPFree.image : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {s A : Set α} {t : Set β} {f : α → β},
  IsMulFreimanIso 2 s t f → A ⊆ s → ThreeGPFree A → ThreeGPFree (f '' A)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coeFnAddMonoidHom_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M),
  Derivation.coeFnAddMonoidHom D = ⇑D
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.imp_self_simp : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, Q ⊢ₛ P → P ↔ True
-- Init.Data.Nat.Lemmas
Nat.succ_sub_sub_succ : ∀ (n m k : ℕ), n.succ - m - k.succ = n - m - k
-- Mathlib.Condensed.Light.InternallyProjective
Quiver.Hom.op.eq_1 : ∀ {V : Type u_1} [inst : Quiver V] {X Y : V} (f : X ⟶ Y), f.op = Opposite.op f
-- Mathlib.Control.Monad.Cont
ContT.run_map : ∀ {r : Type u} {m : Type u → Type v} {α β : Type w} (f : α → β) (x : ContT r m α) (k : β → m r),
  (f <$> x).run k = x.run (k ∘ f)
-- Mathlib.Order.Circular
SBtw.mk : {α : Type u_1} → (α → α → α → Prop) → SBtw α
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.prod_fintype_slash : ∀ {ι : Type u_1} [inst : Fintype ι] [Nonempty ι] {k : ℤ} {g : GL (Fin 2) ℝ} {f : ι → UpperHalfPlane → ℂ},
  SlashAction.map (k * ↑(Fintype.card ι)) g (∏ i, f i) =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ (Fintype.card ι - 1) • ∏ i, SlashAction.map k g (f i)
-- Lean.Meta.Match.CaseArraySizes
Lean.Meta.CaseArraySizesSubgoal.mvarId : Lean.Meta.CaseArraySizesSubgoal → Lean.MVarId
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atBot : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : ProbabilityTheory.IsMeasurableRatCDF f) (a : α),
  Filter.Tendsto (↑(hf.stieltjesFunction a)) Filter.atBot (nhds 0)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.SupportsStmt.eq_def : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (S : Finset Λ) (x : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.SupportsStmt S x =
    match x with
    | Turing.TM2.Stmt.push k a q => Turing.TM2.SupportsStmt S q
    | Turing.TM2.Stmt.peek k a q => Turing.TM2.SupportsStmt S q
    | Turing.TM2.Stmt.pop k a q => Turing.TM2.SupportsStmt S q
    | Turing.TM2.Stmt.load a q => Turing.TM2.SupportsStmt S q
    | Turing.TM2.Stmt.branch a q₁ q₂ => Turing.TM2.SupportsStmt S q₁ ∧ Turing.TM2.SupportsStmt S q₂
    | Turing.TM2.Stmt.goto l => ∀ (v : σ), l v ∈ S
    | Turing.TM2.Stmt.halt => True
-- Mathlib.Algebra.Star.Pointwise
Set.image_star : ∀ {α : Type u_1} {s : Set α} [inst : InvolutiveStar α], star '' s = star s
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.toList_ric : ∀ {α : Type u} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => Unit),
  t.Ordered →
    ∀ (bound : α),
      Std.Slice.toList (Std.Ric.Sliceable.mkSlice t *...=bound) = List.filter (fun e => (compare e bound).isLE) t.keys
-- Mathlib.Order.Filter.Pointwise
Filter.le_sub_iff : ∀ {α : Type u_2} [inst : Sub α] {f g h : Filter α}, h ≤ f - g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s - t ∈ h
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instMonoidalPreadditive : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G],
  CategoryTheory.MonoidalPreadditive (Rep.{u, u, v} k G)
-- Mathlib.Algebra.Ring.Prod
NonUnitalRingHom.prodMap_def : ∀ {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] [inst_2 : NonUnitalNonAssocSemiring R'] [inst_3 : NonUnitalNonAssocSemiring S']
  (f : R →ₙ+* R') (g : S →ₙ+* S'),
  f.prodMap g = (f.comp (NonUnitalRingHom.fst R S)).prod (g.comp (NonUnitalRingHom.snd R S))
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryLTD : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → (a : α) × β a → (a : α) × β a