mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.normLeOne.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (a a_1 : NumberField.mixedEmbedding.mixedSpace K),
  a = a_1 →
    NumberField.mixedEmbedding.fundamentalCone.normLeOne K a =
      NumberField.mixedEmbedding.fundamentalCone.normLeOne K a_1
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
prodIsoPullback_inv_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y]
  {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).inv
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X)
        (CategoryTheory.Limits.terminal.from Y))
      h
-- Mathlib.Data.EReal.Basic
EReal.coe_lt_top : ∀ (x : ℝ), ↑x < ⊤
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_set_pi : ∀ {G : Type u_5} {ι : Type u_6} {α : ι → Type u_7} [inst : AddGroup G] [inst_1 : (i : ι) → AddAction G (α i)] (c : G)
  (I : Set ι) (s : (i : ι) → Set (α i)), c +ᵥ I.pi s = I.pi (c +ᵥ s)
-- Mathlib.RingTheory.Polynomial.Pochhammer
monic_ascPochhammer : ∀ (S : Type u) [inst : Semiring S] (n : ℕ) [Nontrivial S] [NoZeroDivisors S], (ascPochhammer S n).Monic
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- A measurable space is a space equipped with a σ-algebra.  -/
MeasurableSpace : Type u_7 → Type u_7
-- Mathlib.Topology.Separation.CompletelyRegular
completelyRegularSpace_iInf : ∀ {ι : Type u_1} {X : Type u_2} {t : ι → TopologicalSpace X},
  (∀ (i : ι), CompletelyRegularSpace X) → CompletelyRegularSpace X
-- Mathlib.SetTheory.Cardinal.Regular
/-- An inaccessible cardinal is uncountable.  -/
Cardinal.IsInaccessible.aleph0_lt : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → Cardinal.aleph0 < c
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.inverseAssociator_obj : ∀ (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] (X : C × D × E),
  (CategoryTheory.prod.inverseAssociator C D E).obj X = ((X.1, X.2.1), X.2.2)
-- Init.Data.ByteArray.Basic
ByteArray.instHashable : Hashable ByteArray
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_lieSpan_submodule_eq_iff : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {p : Submodule R M},
  ↑(LieSubmodule.lieSpan R L ↑p) = p ↔ ∃ N, ↑N = p
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.equivalenceJ_inverse : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) {X₂ : C₂}
  {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), (w.equivalenceJ g).inverse = CategoryTheory.TwoSquare.EquivalenceJ.inverse w g
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivAtFilter_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] (L : Filter (E × E)), HasFDerivAtFilter id (ContinuousLinearMap.id 𝕜 E) L
-- Mathlib.Algebra.Order.Ring.GeomSum
geom_sum_eq_zero_iff_neg_one : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R},
  n ≠ 0 → (∑ i ∈ Finset.range n, x ^ i = 0 ↔ x = -1 ∧ Even n)
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.piCongrRight_refl : ∀ {η : Type u_16} {Ms : η → Type u_17} [inst : (j : η) → Mul (Ms j)],
  (MulEquiv.piCongrRight fun j => MulEquiv.refl (Ms j)) = MulEquiv.refl ((j : η) → Ms j)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- The relation on `FreeAddMonoid (R × Π i, s i)` that generates a congruence whose quotient is
the tensor product.  -/
PiTensorProduct.Eqv : {ι : Type u_1} →
  (R : Type u_4) →
    [inst : CommSemiring R] →
      (s : ι → Type u_7) →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [(i : ι) → Module R (s i)] → FreeAddMonoid (R × ((i : ι) → s i)) → FreeAddMonoid (R × ((i : ι) → s i)) → Prop
-- Mathlib.Order.SuccPred.Limit
/-- A value can be built by building it on predecessors and predecessor pre-limits.  -/
Order.isPredPrelimitRecOn : {α : Type u_1} →
  (b : α) →
    {motive : α → Sort u_2} →
      [inst : PartialOrder α] →
        [inst_1 : PredOrder α] →
          ((a : α) → ¬IsMin a → motive (Order.pred a)) → ((a : α) → Order.IsPredPrelimit a → motive a) → motive b
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.closedBall_eq_of_mem : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] {x y : X} {r : ℝ},
  y ∈ Metric.closedBall x r → Metric.closedBall x r = Metric.closedBall y r
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.PublishDiagnosticsParams.mk.inj : ∀ {uri : Lean.Lsp.DocumentUri} {version? : Option ℤ} {isIncremental? : Option Bool}
  {diagnostics : Array Lean.Lsp.Diagnostic} {uri_1 : Lean.Lsp.DocumentUri} {version?_1 : Option ℤ}
  {isIncremental?_1 : Option Bool} {diagnostics_1 : Array Lean.Lsp.Diagnostic},
  { uri := uri, version? := version?, isIncremental? := isIncremental?, diagnostics := diagnostics } =
      { uri := uri_1, version? := version?_1, isIncremental? := isIncremental?_1, diagnostics := diagnostics_1 } →
    uri = uri_1 ∧ version? = version?_1 ∧ isIncremental? = isIncremental?_1 ∧ diagnostics = diagnostics_1
-- Batteries.Data.AssocList
List.toAssocList.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (a : α) (b : β) (es : List (α × β)),
  ((a, b) :: es).toAssocList = Batteries.AssocList.cons a b es.toAssocList
-- Mathlib.RingTheory.LocalRing.LocalSubring
/-- The underlying subring of a local subring.  -/
LocalSubring.toSubring : {R : Type u_1} → [inst : CommRing R] → LocalSubring R → Subring R
-- Mathlib.Tactic.Linarith.Preprocessing
/-- `removeNeAux` case splits on any proof `h : a ≠ b` in the input,
turning it into `a < b ∨ a > b`, provided the type has a `LinearOrder` instance.
This produces `2^n` branches when there are `n` such hypotheses in the input.
 -/
Mathlib.Tactic.Linarith.removeNeAux : Lean.MVarId → List Lean.Expr → Lean.MetaM (List Mathlib.Tactic.Linarith.Branch)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- An arbitrary isomorphism from `ZMod n` to any cyclic additive group of `Nat.card` equal to `n`.
See `zmodAddCyclicAddEquiv` for a version which doesn't require an explicit generator,
and instead picks one out with the axiom of choice.  -/
zmodAddCyclicAddEquiv : {G : Type u_2} → [inst : AddGroup G] → IsAddCyclic G → ZMod (Nat.card G) ≃+ G
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
/-- The `characterSpace 𝕜 A` along with `0` is always a closed set in `WeakDual 𝕜 A`.  -/
WeakDual.CharacterSpace.union_zero_isClosed : ∀ (𝕜 : Type u_1) (A : Type u_2) [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : TopologicalSpace A]
  [inst_6 : Module 𝕜 A] [T2Space 𝕜] [ContinuousMul 𝕜], IsClosed (WeakDual.characterSpace 𝕜 A ∪ {0})
-- Mathlib.Data.Finsupp.Order
Finsupp.mapDomain_le_mapDomain_iff_le : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : LE α] [Std.Refl fun x1 x2 => x1 ≤ x2]
  {f : ι → κ}, Function.Injective f → ∀ (g₁ g₂ : ι →₀ α), Finsupp.mapDomain f g₁ ≤ Finsupp.mapDomain f g₂ ↔ g₁ ≤ g₂
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabSetOption : Lean.Elab.Term.TermElab
-- Lean.Meta.Constructions.NoConfusion
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.withEqTelescope.go : {α : Type} →
  Array Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → List Lean.Expr → List Lean.Expr → Array Lean.Expr → Lean.MetaM α
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewFact.fact.inj : ∀ {prop proof : Lean.Expr} {generation : ℕ} {prop_1 proof_1 : Lean.Expr} {generation_1 : ℕ},
  Lean.Meta.Grind.NewFact.fact prop proof generation = Lean.Meta.Grind.NewFact.fact prop_1 proof_1 generation_1 →
    prop = prop_1 ∧ proof = proof_1 ∧ generation = generation_1
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.mapsTo_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  Set.MapsTo (↑e.symm) e.target e.source
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.quotientPi_aux.invFun : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {Ms : ι → Type u_3} →
        [inst_1 : (i : ι) → AddCommGroup (Ms i)] →
          [inst_2 : (i : ι) → Module R (Ms i)] →
            (p : (i : ι) → Submodule R (Ms i)) →
              [Fintype ι] → [DecidableEq ι] → ((i : ι) → Ms i ⧸ p i) → ((i : ι) → Ms i) ⧸ Submodule.pi Set.univ p
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insertIfNew k v).maxKey? = some (t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k')
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.tsupport_subset' : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} (self : TestFunction Ω F n),
  tsupport self.toFun ⊆ ↑Ω
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_pos : ∀ {r : ENNReal}, 0 < ⌈r⌉ₑ ↔ 0 < r
-- Lean.Environment
_private.Lean.Environment.0.Lean.readIRPartsOfMod : Lean.Name → IO (Array (Lean.ModuleData × Lean.CompactedRegion))
-- Mathlib.Algebra.Free
instReprFreeAddMagma.eq_1 : ∀ {α : Type u} [inst : Repr α], instReprFreeAddMagma = { reprPrec := fun o x => o.repr }
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : α →*₀ β),
  (MonoidWithZeroHom.id β).comp f = f
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
/-- **Alias** of the forward direction of `SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton`. -/
SimpleGraph.EdgeDisjointTriangles.mem_sym2_subsingleton : ∀ {α : Type u_1} {G : SimpleGraph α},
  G.EdgeDisjointTriangles → ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}.Subsingleton
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.unifIntegrable_congr_ae : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {f g : ι → α → β},
  (∀ (n : ι), f n =ᵐ[μ] g n) → (MeasureTheory.UnifIntegrable f p μ ↔ MeasureTheory.UnifIntegrable g p μ)
-- Batteries.Util.ExtendedBinder
/-- The syntax `∃ᵉ (x < 2) (y < 3), p x y` is shorthand for `∃ x < 2, ∃ y < 3, p x y`.  -/
Batteries.ExtendedBinder.«term∃ᵉ_,_» : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens)
  (x : ↑(Y.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).hom)
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) x) =
    (CategoryTheory.ConcreteCategory.hom (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op)) x
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstFieldDeclParser.formatter : optParam ℕ 0 → Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Binomial
/-- Pochhammer version of Chu-Vandermonde identity  -/
Ring.descPochhammer_smeval_add : ∀ {R : Type u_1} [inst : Ring R] {r s : R} (k : ℕ),
  Commute r s →
    (descPochhammer ℤ k).smeval (r + s) =
      ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal k,
        ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
-- Mathlib.Logic.Equiv.Array
/-- If `α` is encodable, then so is `Array α`.  -/
Array.encodable : {α : Type u_1} → [Encodable α] → Encodable (Array α)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size
-- Mathlib.Topology.Connected.PathComponentOne
OpenNormalSubgroup.instIsClosedCoePathComponentOne : ∀ (G : Type u_1) [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : LocallyPathConnectedSpace G], IsClosed ↑(OpenNormalSubgroup.pathComponentOne G)
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- The automorphism of the polynomial algebra given by `p(X) ↦ p(X+t)`,
with inverse `p(X) ↦ p(X-t)`.  -/
Polynomial.algEquivAevalXAddC : {R : Type u_3} → [inst : CommRing R] → R → Polynomial R ≃ₐ[R] Polynomial R
-- Mathlib.AlgebraicGeometry.Scheme
/-- The spectrum, as a contravariant functor from commutative rings to schemes.  -/
AlgebraicGeometry.Scheme.Spec : CategoryTheory.Functor CommRingCatᵒᵖ AlgebraicGeometry.Scheme
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.eq_of_monic_of_associated : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.Monic → q.Monic → Associated p q → p = q
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- The algebra equivalence between `MonoidAlgebra` and `AddMonoidAlgebra` in terms of
`Additive`.  -/
MonoidAlgebra.toAdditiveAlgEquiv : (R : Type u_1) →
  (A : Type u_4) →
    (M : Type u_7) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : Monoid M] → MonoidAlgebra A M ≃ₐ[R] AddMonoidAlgebra A (Additive M)
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
/-- **Alias** of the forward direction of `Matrix.nondegenerate_iff_det_ne_zero`. -/
Matrix.Nondegenerate.det_ne_zero : ∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} [inst_1 : CommRing A] [IsDomain A] {M : Matrix n n A}
  [inst_3 : DecidableEq n], M.Nondegenerate → M.det ≠ 0
-- Mathlib.RepresentationTheory.FiniteIndex
/-- Let `S ≤ G` be a finite index subgroup, `g₁, ..., gₙ` a set of right coset representatives of
`S`, and `A` a `k`-linear `S`-representation. This is the `k`-linear map
`Coind_S^G(A) →ₗ[k] Ind_S^G(A)` sending `f : G → A` to `∑ᵢ ⟦gᵢ ⊗ₜ[k] f(gᵢ)⟧` for `1 ≤ i ≤ n`.  -/
Rep.coindToInd : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        {S : Subgroup G} →
          (A : Rep.{w, u, v} k ↥S) →
            [S.FiniteIndex] → ↑(Rep.coind.{u, v, v, w} S.subtype A) →ₗ[k] ↑(Rep.ind S.subtype A)
-- Mathlib.Analysis.Complex.BorelCaratheodory
/-- If `z.re ≤ M`, then `‖z‖ ≤ ‖2M - z‖`. This shows that the Schwarz transform
`z ↦ z / (2M - z)` has numerator smaller than denominator when the real part is bounded by M  -/
_private.Mathlib.Analysis.Complex.BorelCaratheodory.0.Complex.norm_le_norm_two_mul_sub : ∀ {M : ℝ} {z : ℂ}, 0 < M → z.re ≤ M → ‖z‖ ≤ ‖2 * ↑M - z‖
-- Mathlib.Order.Lattice
SemilatticeInf.toPartialOrder : {α : Type u} → [self : SemilatticeInf α] → PartialOrder α
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ringHomComp_eq_one_iff : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {R'' : Type u_3} [inst_2 : CommRing R'']
  {f : R' →+* R''}, Function.Injective ⇑f → ∀ {χ : MulChar R R'}, χ.ringHomComp f = 1 ↔ χ = 1
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight₁_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K], Height.mulHeight₁ 1 = 1
-- Mathlib.Analysis.Normed.Ring.Basic
NormedRing.toMetricSpace : {α : Type u_5} → [self : NormedRing α] → MetricSpace α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullbackConeOfRightIso_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g],
  (CategoryTheory.Limits.pullbackConeOfRightIso f g).snd = CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv g)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Function.Injective.mulActionHom_embedding_isInjective : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : Group H] [inst_3 : MulAction H β] {σ : G → H} {f : α →ₑ[σ] β} {ι : Type u_5} (hf : Function.Injective ⇑f),
  Function.Injective ⇑(Function.Injective.mulActionHom_embedding ι hf)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] {X Y : C} {f : X ⟶ Y}
  (toTransfiniteCompositionOfShape : CategoryTheory.TransfiniteCompositionOfShape J f)
  (map_mem : ∀ (j : J), ¬IsMax j → W (toTransfiniteCompositionOfShape.F.map (CategoryTheory.homOfLE ⋯)))
  (toTransfiniteCompositionOfShape_1 : CategoryTheory.TransfiniteCompositionOfShape J f)
  (map_mem_1 : ∀ (j : J), ¬IsMax j → W (toTransfiniteCompositionOfShape_1.F.map (CategoryTheory.homOfLE ⋯))),
  ({ toTransfiniteCompositionOfShape := toTransfiniteCompositionOfShape, map_mem := map_mem } =
      { toTransfiniteCompositionOfShape := toTransfiniteCompositionOfShape_1, map_mem := map_mem_1 }) =
    (toTransfiniteCompositionOfShape = toTransfiniteCompositionOfShape_1)
-- Mathlib.Order.Monotone.Basic
StrictMonoOn.compares : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → ∀ {o : Ordering}, o.Compares (f a) (f b) ↔ o.Compares a b
-- Lean.Elab.Tactic.RCases
/-- Given a list of targets of the form `e` or `h : e`, and a pattern, match all the targets
against the pattern. Returns the list of produced subgoals.
 -/
Lean.Elab.Tactic.RCases.rcases : Array (Option Lean.Ident × Lean.Syntax) →
  Lean.Elab.Tactic.RCases.RCasesPatt → Lean.MVarId → Lean.Elab.TermElabM (List Lean.MVarId)
-- Lean.Expr
/-- `e.foldlM f a` folds the monadic function `f` over the subterms of the expression `e`,
with initial value `a`.  -/
Lean.Expr.foldlM : {α : Type} → {m : Type → Type u_1} → [Monad m] → (α → Lean.Expr → m α) → α → Lean.Expr → m α
-- Init.Data.Array.Find
Array.find?_flatMap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {p : β → Bool},
  Array.find? p (Array.flatMap f xs) = Array.findSome? (fun x => Array.find? p (f x)) xs
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.isColimitOfIsos.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {X' Y' : C}
  (c : CategoryTheory.Limits.Cofork f g) (hc hc_1 : CategoryTheory.Limits.IsColimit c),
  hc = hc_1 →
    ∀ {f' g' : X' ⟶ Y'} (c' : CategoryTheory.Limits.Cofork f' g') (e₀ e₀_1 : X ≅ X') (e_e₀ : e₀ = e₀_1)
      (e₁ e₁_1 : Y ≅ Y') (e_e₁ : e₁ = e₁_1) (e e_1 : c.pt ≅ c'.pt) (e_e : e = e_1)
      (comm₁ : CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom)
      (comm₂ : CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom)
      (comm₃ : CategoryTheory.CategoryStruct.comp e₁.inv (CategoryTheory.CategoryStruct.comp c.π e.hom) = c'.π),
      c.isColimitOfIsos hc c' e₀ e₁ e comm₁ comm₂ comm₃ = c.isColimitOfIsos hc_1 c' e₀_1 e₁_1 e_1 ⋯ ⋯ ⋯
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
/-- The normalised Eisenstein series of weight `2` and level `1`.
Defined as `(1 / 2 * ζ(2)) * G2 `.  -/
EisensteinSeries.E2 : UpperHalfPlane → ℂ
-- Lean.Meta.Tactic.Grind.Types
/-- Each E-node may have "solver terms" attached to them.
Each term is an element of the equivalence class that the
solver cares about. Each solver is responsible for marking the terms they care about.
The `grind` core propagates equalities and disequalities to the theory solvers
using these "marked" terms. The root of the equivalence class
contains a list of representatives sorted by solver id. Note that many E-nodes
do not have any solver terms attached to them.

"Solver terms" are referenced as "theory variables" in the SMT literature.
The SMT solver Z3 uses a similar representation.
 -/
Lean.Meta.Grind.SolverTerms : Type
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.equivAlgHom_symm_apply_val : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [inst_6 : Algebra R R']
  [inst_7 : Algebra S S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  (f : { f // ∀ (x : P.Ring), (MvPolynomial.aeval P'.val) (f x) = (algebraMap S S') ((MvPolynomial.aeval P.val) x) })
  (i : ι), (Algebra.Generators.Hom.equivAlgHom.symm f).val i = ↑f (MvPolynomial.X i)
-- Init.Data.Ord.Basic
Ordering.instLawfulIdentityThenEq : Std.LawfulIdentity Ordering.then Ordering.eq
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.inhabited : (F : PFunctor.{uA, uB}) → [Inhabited F.A] → Inhabited F.M
-- Init.Data.List.Sublist
List.suffix_refl : ∀ {α : Type u_1} (l : List α), l <:+ l
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_fiberwise : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq κ] [inst_2 : Fintype κ]
  (s : Finset ι) (g : ι → κ) (f : ι → M), ∑ j, ∑ i ∈ s with g i = j, f i = ∑ i ∈ s, f i
-- Mathlib.Data.Vector.Defs
/-- The first element of a vector with length at least `1`.  -/
List.Vector.head : {α : Type u_1} → {n : ℕ} → List.Vector α n.succ → α
-- Lean.MonadEnv
Lean.matchConstCtor : {m : Type → Type} →
  {α : Type} →
    [Monad m] → [Lean.MonadEnv m] → Lean.Expr → (Unit → m α) → (Lean.ConstructorVal → List Lean.Level → m α) → m α
-- Mathlib.Algebra.Order.Ring.Int
Int.instIsStrictOrderedRing : IsStrictOrderedRing ℤ
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- If `entry.previous.isSome`, then replace it with `none`, and add the required entries
to `entry.stack`.
 -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.processPrevious : Lean.Meta.RefinedDiscrTree.LazyEntry → Lean.MetaM Lean.Meta.RefinedDiscrTree.LazyEntry
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitInclusiveIterator.toOption.match_1.splitter : {ρ : Type} →
  {σ : String.Slice → Type} →
    {pat : ρ} →
      [inst : String.Slice.Pattern.ToForwardSearcher pat σ] →
        {s : String.Slice} →
          (motive : String.Slice.SplitInclusiveIterator pat s → Sort u_1) →
            (x : String.Slice.SplitInclusiveIterator pat s) →
              ((currPos : s.Pos) →
                  (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                    motive (String.Slice.SplitInclusiveIterator.operating currPos s_1)) →
                (Unit → motive String.Slice.SplitInclusiveIterator.atEnd) → motive x
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonResolveSupport.toJson : Lean.Lsp.ResolveSupport → Lean.Json
-- Mathlib.Algebra.Torsor.Basic
Prod.snd_vsub : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup G']
  [inst_2 : AddTorsor G P] [inst_3 : AddTorsor G' P'] (p₁ p₂ : P × P'), (p₁ -ᵥ p₂).2 = p₁.2 -ᵥ p₂.2
-- Std.Time.Date.Unit.Month
Std.Time.Month.instOrdOffset : Ord Std.Time.Month.Offset
-- Mathlib.Data.Fintype.Perm
AddEquiv.instFintype : {α : Type u_4} →
  {β : Type u_5} →
    [inst : Add α] → [inst_1 : Add β] → [DecidableEq α] → [DecidableEq β] → [Fintype α] → [Fintype β] → Fintype (α ≃+ β)