mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.PerfectPairing.Restrict
/-- An auxiliary definition used only to simplify the construction of the more general definition
`PerfectPairing.restrictScalarsField`.  -/
_private.Mathlib.LinearAlgebra.PerfectPairing.Restrict.0.LinearMap.restrictScalars_field_aux : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module L M] [inst_6 : Module L N] [inst_7 : Module K M]
  [inst_8 : Module K N] [inst_9 : IsScalarTower K L M] (p : M →ₗ[L] N →ₗ[L] L) [p.IsPerfPair] {M' : Type u_5}
  {N' : Type u_6} [inst_11 : AddCommGroup M'] [inst_12 : AddCommGroup N'] [inst_13 : Module K M']
  [inst_14 : Module K N'] [inst_15 : IsScalarTower K L N] (i : M' →ₗ[K] M) (j : N' →ₗ[K] N),
  Function.Injective ⇑i →
    Function.Injective ⇑j →
      Submodule.span L ↑i.range = ⊤ →
        Submodule.span L ↑j.range = ⊤ →
          ∀ (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range),
            (i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp).IsPerfPair
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Fintype.mem_span_image_iff_exists_fun : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M} {x : M} {s : Set α} [inst_3 : Fintype ↑s], x ∈ Submodule.span R (v '' s) ↔ ∃ c, ∑ i, c i • v ↑i = x
-- Mathlib.Algebra.Category.MonCat.Yoneda
AddCommMonCat.coyoneda.eq_1 : AddCommMonCat.coyoneda =
  {
    obj := fun M =>
      { obj := fun N => AddCommMonCat.of (↑(Opposite.unop M) →+ ↑N),
        map := fun {X Y} f => AddCommMonCat.ofHom (AddMonoidHom.compHom (AddCommMonCat.Hom.hom f)), map_id := ⋯,
        map_comp := ⋯ },
    map := fun {X Y} f =>
      { app := fun N => AddCommMonCat.ofHom (AddCommMonCat.Hom.hom f.unop).compHom', naturality := ⋯ },
    map_id := AddCommMonCat.coyoneda._proof_4, map_comp := @AddCommMonCat.coyoneda._proof_5 }
-- Mathlib.Order.WithBot
WithBot.IsWellOrder.gt : ∀ {α : Type u_1} [inst : Preorder α] [IsWellOrder α fun x1 x2 => x1 > x2], IsWellOrder (WithBot α) fun x1 x2 => x1 > x2
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.homotopyEquiv_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  (hc : ∀ (i : α), ∃ j, c.Rel i j),
  (HomologicalComplex.pathObject.homotopyEquiv K hc).inv = HomologicalComplex.pathObject.π₀ K
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.order_single_mul_of_isRegular : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {g : Γ} {r : R},
  IsRegular r → ∀ {x : HahnSeries Γ R}, x ≠ 0 → ((HahnSeries.single g) r * x).order = g + x.order
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.lift_f_fst_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α : M ⟶ K) (β : CochainComplex.HomComplex.Cochain M L (-1))
  (hαβ :
    CochainComplex.HomComplex.δ (-1) 0 β +
        CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) =
      0)
  (p : ℤ),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.lift φ α β hαβ).f p)
      ((CochainComplex.mappingCocone.fst φ).f p) =
    α.f p
-- Mathlib.Topology.UniformSpace.Equiv
/-- Inverse of a uniform isomorphism.  -/
UniformEquiv.symm : {α : Type u} → {β : Type u_1} → [inst : UniformSpace α] → [inst_1 : UniformSpace β] → α ≃ᵤ β → β ≃ᵤ α
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelπ.epi : ∀ {X Y : SemiNormedGrp} {f : X ⟶ Y}, CategoryTheory.Epi (SemiNormedGrp.explicitCokernelπ f)
-- Mathlib.Data.Complex.Basic
Complex.normSq_div : ∀ (z w : ℂ), Complex.normSq (z / w) = Complex.normSq z / Complex.normSq w
-- Mathlib.MeasureTheory.MeasurableSpace.Card
MeasurableSpace.generateMeasurableRec_omega_one : ∀ {α : Type u} (s : Set (Set α)),
  MeasurableSpace.generateMeasurableRec s (Ordinal.omega 1) =
    ⋃ i, ⋃ (_ : i < Ordinal.omega 1), MeasurableSpace.generateMeasurableRec s i
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightUnshift_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ)
  (hn : n' + a = n) (p q : ℤ) (hpq : p + n = q) (p' : ℤ) (hp' : p + n' = p'),
  (γ.rightUnshift n hn).v p q hpq =
    CategoryTheory.CategoryStruct.comp (γ.v p p' hp') (L.shiftFunctorObjXIso a p' q ⋯).hom
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.lim.congr_simp : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [inst_5 : CauSeq.IsComplete β abv]
  (s s_1 : CauSeq β abv), s = s_1 → s.lim = s_1.lim
-- Mathlib.Algebra.Group.Subgroup.Basic
ConjClasses.mem_noncenter : ∀ {G : Type u_6} [inst : Monoid G] (g : ConjClasses G), g ∈ ConjClasses.noncenter G ↔ g.carrier.Nontrivial
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- A submodule of a finite module is CoFG.  -/
Submodule.CoFG.of_finite : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  {S : Submodule R M}, S.CoFG
-- Lean.Meta.Tactic.Grind.Extension
/-- The actual `rhs`.  -/
Lean.Meta.Grind.CnstrRHS.expr : Lean.Meta.Grind.CnstrRHS → Lean.Expr
-- Mathlib.Dynamics.Ergodic.Ergodic
Ergodic.zero_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α}, Measurable f → Ergodic f 0
-- Mathlib.ModelTheory.Order
FirstOrder.Language.sum.instIsOrdered : {L : FirstOrder.Language} → (L.sum FirstOrder.Language.order).IsOrdered
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.instLawfulUpwardEnumerableLT : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {β : Type v} [inst_2 : LE β] [inst_3 : LT β]
  [inst_4 : Std.PRange.UpwardEnumerable β] [inst_5 : Std.PRange.LawfulUpwardEnumerable β]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] [m : HasModel✝ α β],
  Std.PRange.LawfulUpwardEnumerableLT α
-- Mathlib.Order.Lattice
Prod.mk_inf_mk : ∀ (α : Type u) (β : Type v) [inst : Min α] [inst_1 : Min β] (a₁ a₂ : α) (b₁ b₂ : β),
  (a₁, b₁) ⊓ (a₂, b₂) = (a₁ ⊓ a₂, b₁ ⊓ b₂)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.trans_smul : ∀ {S : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {G : Type u_5} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : Module S V]
  [inst_6 : ContinuousConstSMul S V] [inst_7 : AddCommMonoid W] [inst_8 : Module R W] [inst_9 : TopologicalSpace W]
  [inst_10 : Module S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : AddCommMonoid G] [inst_13 : Module R G]
  [inst_14 : TopologicalSpace G] [inst_15 : Module S G] [inst_16 : ContinuousConstSMul S G]
  [inst_17 : SMulCommClass R S W] [inst_18 : SMul S R] [inst_19 : IsScalarTower S R V] [inst_20 : IsScalarTower S R W]
  [inst_21 : IsScalarTower S R G] (α : Sˣ) (e : G ≃L[R] V) (f : V ≃L[R] W), e.trans (α • f) = α • e.trans f
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.nil_drop_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ), (p.drop n).Nil ↔ p.length ≤ n
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singleton_sub_singleton : ∀ {α : Type u_2} [inst : Sub α] {a b : α}, {a} - {b} = {a - b}
-- Init.Data.List.MinMaxOn
List.apply_minOn_lt_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLT β] {xs : List α} {f : α → β} (h : xs ≠ []) {b : β}, f (List.minOn f xs h) < b ↔ ∃ x ∈ xs, f x < b
-- Mathlib.GroupTheory.Complement
Subgroup.RightTransversal.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.RightTransversal = { T // Subgroup.IsComplement (↑H) T }
-- Mathlib.MeasureTheory.Measure.AEMeasurable
nullMeasurableSet_eq_fun : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [MeasurableEq β] {f g : α → β},
  AEMeasurable f μ → AEMeasurable g μ → MeasureTheory.NullMeasurableSet {x | f x = g x} μ
-- Mathlib.GroupTheory.GroupAction.Support
AddAction.Supports.vadd : ∀ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [inst : AddGroup H] [inst_1 : VAdd G α]
  [inst_2 : VAdd G β] [inst_3 : AddAction H α] [inst_4 : VAdd H β] [VAddCommClass G H β] [VAddCommClass G H α]
  {s : Set α} {b : β} (g : H), AddAction.Supports G s b → AddAction.Supports G (g +ᵥ s) (g +ᵥ b)
-- Init.Data.Ord.Basic
List.compareLex_nil_left_eq_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering} {xs : List α}, List.compareLex cmp [] xs = Ordering.eq ↔ xs = []
-- Init.Data.Bool
Bool.lt_of_lt_of_le : ∀ {x y z : Bool}, x < y → y ≤ z → x < z
-- Std.Async.System
Std.Async.System.instReprGroupId : Repr Std.Async.System.GroupId
-- Mathlib.Order.Defs.Unbundled
/-- `IsAntisymm X r` means the binary relation `r` on `X` is antisymmetric.  -/
IsAntisymm : (α : Sort u_1) → (α → α → Prop) → Prop
-- Mathlib.Algebra.CharP.Two
CharTwo.add_sq : ∀ {R : Type u_1} [inst : CommSemiring R] [CharP R 2] (x y : R), (x + y) ^ 2 = x ^ 2 + y ^ 2
-- Mathlib.Analysis.Analytic.Constructions
/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic.  -/
AnalyticOnNhd.pow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_7} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : E → A}
  {s : Set E}, AnalyticOnNhd 𝕜 f s → ∀ (n : ℕ), AnalyticOnNhd 𝕜 (f ^ n) s
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.toNorm_coe : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {p : ENNReal} (x : ↥(lp E p)) (i : α),
  ↑(lp.toNorm x) i = ‖↑x i‖
-- Init.Data.Option.Monadic
Option.elimM_pure : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] (x : Option α) (y : m β) (z : α → m β),
  Option.elimM (pure x) y z = x.elim y z
-- Mathlib.CategoryTheory.Limits.Creates
/-- the lifted cocone is colimit  -/
CategoryTheory.LiftsToColimit.makesColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                {c : CategoryTheory.Limits.Cocone (K.comp F)} →
                  {t : CategoryTheory.Limits.IsColimit c} →
                    (self : CategoryTheory.LiftsToColimit K F c t) → CategoryTheory.Limits.IsColimit self.liftedCocone
-- Batteries.Data.List.Lemmas
List.map_getElem_finRange : ∀ {α : Type u_1} (l : List α), List.map (fun x => l[↑x]) (List.finRange l.length) = l
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.instIsCorepresentableObjOppositeTypeUliftCoyoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ},
  (CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.obj X).IsCorepresentable
-- Mathlib.Topology.MetricSpace.Thickening
Metric.mem_thickening_iff_infDist_lt : ∀ {δ : ℝ} {X : Type u} [inst : PseudoMetricSpace X] {E : Set X} {x : X},
  E.Nonempty → (x ∈ Metric.thickening δ E ↔ Metric.infDist x E < δ)
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The action by a subfield is the action by the underlying field.  -/
Subfield.instModuleSubtypeMem : {K : Type u} →
  [inst : DivisionRing K] →
    {X : Type u_1} → [inst_1 : AddCommMonoid X] → [Module K X] → (F : Subfield K) → Module (↥F) X
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- Unfold the definition of `dimH` using `[MeasurableSpace X] [BorelSpace X]` from the
environment.  -/
dimH_def : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (s : Set X),
  dimH s = ⨆ d, ⨆ (_ : (MeasureTheory.Measure.hausdorffMeasure ↑d) s = ⊤), ↑d
-- Mathlib.Analysis.Convex.Approximation
/-- The real version of `univ_sSup_affine_eq`.  -/
ConvexOn.real_univ_sSup_affine_eq : ∀ {E : Type u_2} {φ : E → ℝ} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E],
  LowerSemicontinuous φ → ConvexOn ℝ Set.univ φ → sSup {f | f ≤ φ ∧ ∃ l c, f = ⇑l + Function.const E c} = φ
-- Mathlib.RingTheory.NormalClosure
Ring.instFiniteNormalClosure : ∀ (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] [Module.Finite R S] [PerfectField (FractionRing R)]
  [IsDedekindDomain S], Module.Finite S (Ring.NormalClosure R S)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mk₀_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : C) (x : Fin 1),
  (CategoryTheory.ComposableArrows.mk₀ X).obj x = X
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.X_sub_C : ∀ {R : Type u_1} [inst : Ring R] (a : R), (Polynomial.X - Polynomial.C a).Splits
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.pow_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (f : X ⟶ M) (n : ℕ) (g : M ⟶ N)
  [CategoryTheory.IsMonHom g] {Z : C} (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f ^ n) (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g ^ n) h
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_pi_div_four : Real.tan (Real.pi / 4) = 1
-- Mathlib.Order.UpperLower.Basic
isUpperSet_preimage_ofDual_iff : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsUpperSet (⇑OrderDual.ofDual ⁻¹' s) ↔ IsLowerSet s
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.coe_lTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N ≃ₗ[R] P), ↑(LinearEquiv.lTensor M f) = LinearMap.lTensor M ↑f
-- Mathlib.Order.Category.HeytAlg
HeytAlg.id_apply : ∀ (X : HeytAlg) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.id_of : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (a : CategoryTheory.Bicategory.Pith B),
  (CategoryTheory.CategoryStruct.id a).of = CategoryTheory.CategoryStruct.id a.as
-- Mathlib.Data.ZMod.Basic
/-- Any ring homomorphism into `ZMod n` has a right inverse.  -/
ZMod.ringHom_rightInverse : ∀ {n : ℕ} {R : Type u_1} [inst : NonAssocRing R] (f : R →+* ZMod n), Function.RightInverse ZMod.cast ⇑f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α} [inst_3 : Inhabited (β k)], k ∉ m₁ → (m₁ ∩ m₂).get! k = default
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.iSup_torsionBy_eq_torsionBy_prod : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_3}
  {S : Finset ι} {q : ι → R},
  (↑S).Pairwise (Function.onFun IsCoprime q) →
    ⨆ i ∈ S, Submodule.torsionBy R M (q i) = Submodule.torsionBy R M (∏ i ∈ S, q i)
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.IsStableUnderRetracts.instIsClosedUnderIsomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsStableUnderRetracts], P.IsClosedUnderIsomorphisms
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {X Y : C} →
            {f : X ⟶ Y} →
              [inst_3 : SuccOrder J] →
                [inst_4 : WellFoundedLT J] →
                  (F : CategoryTheory.Functor J C) →
                    (isoBot : F.obj ⊥ ≅ X) →
                      autoParam F.IsWellOrderContinuous
                          CategoryTheory.TransfiniteCompositionOfShape.isWellOrderContinuous._autoParam →
                        (incl : F ⟶ (CategoryTheory.Functor.const J).obj Y) →
                          CategoryTheory.Limits.IsColimit { pt := Y, ι := incl } →
                            autoParam (CategoryTheory.CategoryStruct.comp isoBot.inv (incl.app ⊥) = f)
                                CategoryTheory.TransfiniteCompositionOfShape.fac._autoParam →
                              CategoryTheory.TransfiniteCompositionOfShape J f
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : SizeOf R] (asIdeal : Ideal R) (isPrime : asIdeal.IsPrime)
  (ne_bot : asIdeal ≠ ⊥),
  sizeOf { asIdeal := asIdeal, isPrime := isPrime, ne_bot := ne_bot } = 1 + sizeOf asIdeal + sizeOf isPrime
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
FDerivMeasurableAux.isOpen_A : ∀ {𝕜 : 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}
  (L : E →L[𝕜] F) (r ε : ℝ), IsOpen (FDerivMeasurableAux.A f L r ε)
-- Mathlib.Analysis.Normed.Module.FiniteDimension
AffineEquiv.continuous_of_finiteDimensional : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  {PE : Type u_1} {PF : Type u_2} [inst_6 : MetricSpace PE] [inst_7 : NormedAddTorsor E PE] [inst_8 : MetricSpace PF]
  [inst_9 : NormedAddTorsor F PF] [FiniteDimensional 𝕜 E] (f : PE ≃ᵃ[𝕜] PF), Continuous ⇑f
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.intLinear : ∀ {C : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive],
  CategoryTheory.Functor.Linear ℤ F
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.map_mono : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (f : L →ₐ[K] L') {S T : IntermediateField K L},
  S ≤ T → IntermediateField.map f S ≤ IntermediateField.map f T
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.support.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y]
  (D : Function.locallyFinsuppWithin U Y), D.support = Function.support ⇑D
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CochainComplex.mk'.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V)
  (d : X₀ ⟶ X₁)
  (succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp f d = 0),
  CochainComplex.mk' X₀ X₁ d succ' = CochainComplex.mk X₀ X₁ (succ' d).fst d (succ' d).snd.fst ⋯ fun S => succ' S.g
-- Mathlib.Tactic.CongrExclamation
Congr!.Config.mk.inj : ∀ {closePre closePost : Bool} {transparency preTransparency postTransparency : Lean.Meta.TransparencyMode}
  {preferLHS partialApp sameFun : Bool} {maxArgs : Option ℕ}
  {typeEqs etaExpand useCongrSimp beqEq closePre_1 closePost_1 : Bool}
  {transparency_1 preTransparency_1 postTransparency_1 : Lean.Meta.TransparencyMode}
  {preferLHS_1 partialApp_1 sameFun_1 : Bool} {maxArgs_1 : Option ℕ}
  {typeEqs_1 etaExpand_1 useCongrSimp_1 beqEq_1 : Bool},
  { closePre := closePre, closePost := closePost, transparency := transparency, preTransparency := preTransparency,
        postTransparency := postTransparency, preferLHS := preferLHS, partialApp := partialApp, sameFun := sameFun,
        maxArgs := maxArgs, typeEqs := typeEqs, etaExpand := etaExpand, useCongrSimp := useCongrSimp, beqEq := beqEq } =
      { closePre := closePre_1, closePost := closePost_1, transparency := transparency_1,
        preTransparency := preTransparency_1, postTransparency := postTransparency_1, preferLHS := preferLHS_1,
        partialApp := partialApp_1, sameFun := sameFun_1, maxArgs := maxArgs_1, typeEqs := typeEqs_1,
        etaExpand := etaExpand_1, useCongrSimp := useCongrSimp_1, beqEq := beqEq_1 } →
    closePre = closePre_1 ∧
      closePost = closePost_1 ∧
        transparency = transparency_1 ∧
          preTransparency = preTransparency_1 ∧
            postTransparency = postTransparency_1 ∧
              preferLHS = preferLHS_1 ∧
                partialApp = partialApp_1 ∧
                  sameFun = sameFun_1 ∧
                    maxArgs = maxArgs_1 ∧
                      typeEqs = typeEqs_1 ∧ etaExpand = etaExpand_1 ∧ useCongrSimp = useCongrSimp_1 ∧ beqEq = beqEq_1
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.toNonUnitalSubalgebra_inj : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] {S U : NonUnitalStarSubalgebra R A}, S.toNonUnitalSubalgebra = U.toNonUnitalSubalgebra ↔ S = U
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.firstReturn_add : ∀ {p q : DyckWord}, (p + q).firstReturn = if p = 0 then q.firstReturn else p.firstReturn
-- Mathlib.Data.Num.Basic
ZNum.instNeg : Neg ZNum
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_6 : F.Braided] [inst_7 : F'.Braided] (e : F ≅ F')
  (X : CategoryTheory.CommGrp C), ((CategoryTheory.Functor.mapCommGrpNatIso e).inv.app X).hom.hom.hom = e.inv.app X.X
-- Mathlib.Algebra.Order.Kleene
mul_kstar_le_kstar : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a : α}, a * KStar.kstar a ≤ KStar.kstar a
-- Std.Data.DHashMap.Raw
/-- Compares two hash maps using Boolean equality on keys and values.

Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
Std.DHashMap.Raw.beq : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [Hashable α] → [LawfulBEq α] → [(k : α) → BEq (β k)] → Std.DHashMap.Raw α β → Std.DHashMap.Raw α β → Bool
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isSome_getElem?_toList_rio_eq : ∀ {n i : ℕ}, ((*...n).toList[i]?.isSome = true) = (i < n)
-- Mathlib.Analysis.Real.OfDigits
/-- `ofDigits d` is the real number `0.d₀d₁d₂...` in base `b`.
We allow repeating representations like `0.999...` here.  -/
Real.ofDigits : {b : ℕ} → (ℕ → Fin b) → ℝ