mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.mk.sizeOf_spec : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} [inst_2 : SizeOf ι] [inst_3 : SizeOf V] (hom : C ⟶ D)
  (inv : D ⟶ C)
  (homotopyHomInvId : Homotopy (CategoryTheory.CategoryStruct.comp hom inv) (CategoryTheory.CategoryStruct.id C))
  (homotopyInvHomId : Homotopy (CategoryTheory.CategoryStruct.comp inv hom) (CategoryTheory.CategoryStruct.id D)),
  sizeOf { hom := hom, inv := inv, homotopyHomInvId := homotopyHomInvId, homotopyInvHomId := homotopyInvHomId } =
    1 + sizeOf hom + sizeOf inv + sizeOf homotopyHomInvId + sizeOf homotopyInvHomId
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- The bijection between `GammaSets` given by multiplying by an element of `SL(2, ℤ)`.  -/
EisensteinSeries.gammaSetEquiv : {N r : ℕ} →
  (a : Fin 2 → ZMod N) →
    [NeZero r] →
      (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) →
        ↑(EisensteinSeries.gammaSet N r a) ≃
          ↑(EisensteinSeries.gammaSet N r
              (Matrix.vecMul a ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)))
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex)
  (comm : CategoryTheory.CategoryStruct.comp I.ι f = 0) {Z_1 : C} (h : J.cocomplex.X 0 ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (I.cocomplex.d 0 1)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.descHomotopyZeroZero f comm) h) =
    CategoryTheory.CategoryStruct.comp (f.f 0) h
-- Mathlib.Order.CompleteLattice.Lemmas
iSup_inf_le_inf_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (f : ι → α) (a : α), ⨆ i, a ⊓ f i ≤ a ⊓ ⨆ i, f i
-- Mathlib.RepresentationTheory.Irreducible
/-- A representation `ρ` is irreducible if it is non-trivial and has no proper non-trivial
subrepresentations.  -/
Representation.IsIrreducible : {G : Type u_1} →
  {k : Type u_2} →
    {V : Type u_3} →
      [inst : Monoid G] →
        [inst_1 : Field k] → [inst_2 : AddCommGroup V] → [inst_3 : Module k V] → Representation k G V → Prop
-- Mathlib.Algebra.GroupWithZero.Submonoid.CancelMulZero
/-- A submagma with zero of a right cancellative magma with zero inherits right cancellation.  -/
MulZeroMemClass.isRightCancelMulZero : ∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] {S : Type u_2} [inst_2 : SetLike S M₀] [inst_3 : MulMemClass S M₀]
  [inst_4 : ZeroMemClass S M₀] (s : S) [IsRightCancelMulZero M₀], IsRightCancelMulZero ↥s
-- Mathlib.Topology.UnitInterval
projIcc_eq_one : ∀ {x : ℝ}, Set.projIcc 0 1 ⋯ x = 1 ↔ 1 ≤ x
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.fintypeSub.eq_1 : ∀ {α : Type u_2} [inst : Sub α] [inst_1 : DecidableEq α] (s t : Set α) [inst_2 : Fintype ↑s] [inst_3 : Fintype ↑t],
  s.fintypeSub t = Set.fintypeImage2 (fun x1 x2 => x1 - x2) s t
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.rank_eq_one_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : IntermediateField F E},
  Module.rank F ↥K = 1 ↔ K = ⊥
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (t : CategoryTheory.Limits.Cone F) (w : F ≅ G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.lift F t)
      (CategoryTheory.Limits.HasLimit.isoOfNatIso w).hom =
    CategoryTheory.Limits.limit.lift G ((CategoryTheory.Limits.Cone.postcompose w.hom).obj t)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Option.elim.match_1.eq_1 : ∀ {α : Type u_1} {β : Sort u_3} (motive : Option α → β → (α → β) → Sort u_2) (x : α) (x_1 : β) (f : α → β)
  (h_1 : (x : α) → (x_2 : β) → (f : α → β) → motive (some x) x_2 f) (h_2 : (y : β) → (x : α → β) → motive none y x),
  (match some x, x_1, f with
    | some x, x_2, f => h_1 x x_2 f
    | none, y, x => h_2 y x) =
    h_1 x x_1 f
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.Hom.opEquiv_symm_apply : ∀ {V : Type u_1} [inst : Quiver V] {X Y : V} (self : (Opposite.unop (Opposite.op X) ⟶ Opposite.unop (Opposite.op Y))ᵒᵖ),
  Quiver.Hom.opEquiv.symm self = Opposite.unop self
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (w : F ≅ G) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
      (CategoryTheory.Limits.HasColimit.isoOfNatIso w).hom =
    CategoryTheory.CategoryStruct.comp (w.hom.app j) (CategoryTheory.Limits.colimit.ι G j)
-- Mathlib.Algebra.QuaternionBasis
/-- A quaternionic basis on `A` is equivalent to a map from the quaternion algebra to `A`.  -/
QuaternionAlgebra.lift : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R A] →
          {c₁ c₂ c₃ : R} → QuaternionAlgebra.Basis A c₁ c₂ c₃ ≃ (QuaternionAlgebra R c₁ c₂ c₃ →ₐ[R] A)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by inclusion of the first factor.  -/
ContinuousAddMonoidHom.inl : (A : Type u_2) →
  (B : Type u_3) →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → A →ₜ+ A × B
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.IntegrableOn.integrable_indicator : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} {s : Set X},
  μ.IntegrableOn f s → MeasurableSet s → μ.Integrable (s.indicator f)
-- Init.Data.Float.Model.Unpacked.Basic
Float.Model.UnpackedFloat.finite.injEq : ∀ (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (exponent : ℤ) (mantissa_pos : 0 < mantissa)
  (sign_1 : Float.Model.UnpackedFloat.Sign) (mantissa_1 : ℕ) (exponent_1 : ℤ) (mantissa_pos_1 : 0 < mantissa_1),
  (Float.Model.UnpackedFloat.finite sign mantissa exponent mantissa_pos =
      Float.Model.UnpackedFloat.finite sign_1 mantissa_1 exponent_1 mantissa_pos_1) =
    (sign = sign_1 ∧ mantissa = mantissa_1 ∧ exponent = exponent_1)
-- Mathlib.Algebra.Order.Hom.Basic
map_ne_zero_iff_ne_one : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : Group α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [GroupNormClass F α β] (f : F) {x : α}, f x ≠ 0 ↔ x ≠ 1
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.I_re : UpperHalfPlane.I.re = 0
-- Mathlib.Data.List.Zip
List.zipWith_zipWith_right : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} {ε : Type u_4} (f : α → δ → ε) (g : β → γ → δ) (la : List α)
  (lb : List β) (lc : List γ),
  List.zipWith f la (List.zipWith g lb lc) = List.zipWith3 (fun a b c => f a (g b c)) la lb lc
-- Mathlib.CategoryTheory.Galois.EssSurj
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.fintypeQuotientStabilizer : {G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalGroup G] →
        [CompactSpace G] →
          {X : Type u_2} →
            [inst_4 : MulAction G X] →
              [inst_5 : TopologicalSpace X] →
                [ContinuousSMul G X] → [DiscreteTopology X] → (x : X) → Fintype (G ⧸ MulAction.stabilizer G x)
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerivedNatTrans_id : ∀ {C : Type u_3} {D : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (LF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : LF.IsLeftDerivedFunctor α W],
  LF.leftDerivedNatTrans LF α α W (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id LF
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.doublingGamma_eq_Gamma : ∀ {s : ℝ}, 0 < s → s.doublingGamma = Real.Gamma s
-- Mathlib.Order.Defs.Unbundled
total_def : ∀ {α : Sort u_1} {r : α → α → Prop}, Std.Total r ↔ ∀ ⦃a b : α⦄, r a b ∨ r b a
-- Mathlib.Algebra.Order.Archimedean.Basic
archimedean_iff_int_lt : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K],
  Archimedean K ↔ ∀ (x : K), ∃ n, x < ↑n
-- Mathlib.CategoryTheory.Galois.Examples
/-- Complement of the image of a morphism `f : X ⟶ Y` in `FintypeCat`.  -/
CategoryTheory.FintypeCat.imageComplement : {X Y : FintypeCat} → (X ⟶ Y) → FintypeCat
-- Lean.Expr
Lean.Expr.appFn : (e : Lean.Expr) → e.isApp = true → Lean.Expr
-- Mathlib.Data.Sum.Order
Sum.instIrreflLiftRel_mathlib : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Irrefl r] [Std.Irrefl s],
  Std.Irrefl (Sum.LiftRel r s)
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
ContinuousMap.coeFn_toLp : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : CompactSpace α] [inst_5 : MeasureTheory.IsFiniteMeasure μ]
  {𝕜 : Type u_3} [inst_6 : Fact (1 ≤ p)] [inst_7 : NormedRing 𝕜] [inst_8 : Module 𝕜 E] [inst_9 : IsBoundedSMul 𝕜 E]
  (f : C(α, E)), ↑↑((ContinuousMap.toLp p μ 𝕜) f) =ᵐ[μ] ⇑f
-- Mathlib.Topology.Order.ScottTopology
/-- The Scott topology on a partial order is T₀.
 -/
Topology.IsScott.instT0Space : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : TopologicalSpace α] [Topology.IsScott α Set.univ], T0Space α
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.colimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J GrpCat), GrpCat.FilteredColimits.colimit F = GrpCat.of ↑(GrpCat.FilteredColimits.G F)
-- Mathlib.Data.Finsupp.ToDFinsupp
DFinsupp.toFinsupp_single : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] [inst_2 : (m : M) → Decidable (m ≠ 0)] (i : ι)
  (m : M), (fun₀ | i => m).toFinsupp = fun₀ | i => m
-- Mathlib.Data.NNReal.Basic
NNReal.coe_mulIndicator : ∀ {α : Type u_2} (s : Set α) (f : α → NNReal) (a : α), ↑(s.mulIndicator f a) = s.mulIndicator (fun x => ↑(f x)) a
-- Mathlib.Algebra.Group.Submonoid.Units
/-- The units of `S`, packaged as a subgroup of `Mˣ`.  -/
Submonoid.units : {M : Type u_1} → [inst : Monoid M] → Submonoid M → Subgroup Mˣ
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.reindexₐ_symm : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {A : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid A] [inst_4 : Mul A] [inst_5 : Module R A] [inst_6 : Star A] {e : m ≃ n},
  CStarMatrix.reindexₐ R A e.symm = (CStarMatrix.reindexₐ R A e).symm
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
/-- A maximally `Kᵣ₊₁`-free graph is `r`-colorable iff it is complete-multipartite.  -/
SimpleGraph.colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree : ∀ {α : Type u_1} {G : SimpleGraph α} {r : ℕ},
  Maximal (fun H => H.CliqueFree (r + 1)) G → (G.Colorable r ↔ G.IsCompleteMultipartite)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.ext_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : TopologicalSpace.PositiveCompacts α}, s = t ↔ ↑s = ↑t
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.id_comp : ∀ {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₂] [inst_1 : Semiring R₃]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃), LinearMap.id ∘ₛₗ f = f
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeries.eq_def : ∀ (G : Type u_1) [inst : AddGroup G] (n : ℕ),
  AddSubgroup.upperCentralSeries G n = (AddSubgroup.upperCentralSeriesAux G n).fst
-- Mathlib.Topology.Algebra.GroupWithZero
Continuous.div : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  [ContinuousMul G₀] {f g : α → G₀} [inst_4 : TopologicalSpace α],
  Continuous f → Continuous g → (∀ (x : α), g x ≠ 0) → Continuous (f / g)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_map_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → γ} {k k' : α},
  m.getKey? k = some k' →
    Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.map f m) k = Option.map (f k') (Std.ExtDHashMap.Const.get? m k)
-- Mathlib.Data.Ineq
Mathlib.instInhabitedIneq : Inhabited Mathlib.Ineq
-- Mathlib.Analysis.Convolution
/-- Approximate `f ⋆ g` if the support of the `f` is bounded within a ball, and `g` is near `g x₀`
on a ball with the same radius around `x₀`.

This is a special case of `dist_convolution_le'` where `L` is `(•)`, `f` has integral 1 and `f` is
nonnegative.  -/
MeasureTheory.dist_convolution_le : ∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] {g : G → E'} [inst_1 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} [inst_2 : SeminormedAddCommGroup G] [BorelSpace G] [SecondCountableTopology G]
  [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] [inst_7 : NormedSpace ℝ E'] [CompleteSpace E'] {f : G → ℝ} {x₀ : G}
  {R ε : ℝ} {z₀ : E'},
  0 ≤ ε →
    Function.support f ⊆ Metric.ball 0 R →
      (∀ (x : G), 0 ≤ f x) →
        ∫ (x : G), f x ∂μ = 1 →
          MeasureTheory.AEStronglyMeasurable g μ →
            (∀ x ∈ Metric.ball x₀ R, dist (g x) z₀ ≤ ε) →
              dist (MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀) z₀ ≤ ε
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
AlgebraicGeometry.Scheme.pointSmallEtale.congr_simp : ∀ {S : AlgebraicGeometry.Scheme} {Ω : Type u} [inst : Field Ω] [inst_1 : IsSepClosed Ω]
  (s s_1 : AlgebraicGeometry.Spec (CommRingCat.of Ω) ⟶ S),
  s = s_1 → AlgebraicGeometry.Scheme.pointSmallEtale s = AlgebraicGeometry.Scheme.pointSmallEtale s_1
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.ext : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  ⦃f g : L.Hom M N⦄, (∀ (x : M), f x = g x) → f = g
-- Aesop.Rule.Name
Aesop.instInhabitedBuilderName : Inhabited Aesop.BuilderName
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_nnreal_eq_integral_norm_rpow : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  {f : α → E} {p : NNReal},
  p ≠ 0 → MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.lpNorm f (↑p) μ = (∫ (x : α), ‖f x‖ ^ ↑p ∂μ) ^ (↑p)⁻¹
-- Init.Grind.Order
Lean.Grind.Order.lt_le_trans : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α},
  a < b → b ≤ c → a < c
-- Lean.Meta.DiscrTree.Basic
/-- If `vs` contains an element `v'` such that `v == v'`, then replace `v'` with `v`.
Otherwise, push `v`.
See issue #2155
Recall that `BEq α` may not be Lawful.
 -/
_private.Lean.Meta.DiscrTree.Basic.0.Lean.Meta.DiscrTree.insertVal : {α : Type u_1} → [BEq α] → Array α → α → Array α
-- Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} (f h : PowerSeries R) {g : Polynomial R}
  (distinguish : g.IsDistinguishedAt I) (notMem : PowerSeries.constantCoeff h ∉ I) (eq : f = ↑g * h),
  g.degree = ↑(((PowerSeries.map (Ideal.Quotient.mk I)) f).order.lift ⋯)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : SizeOf C] (K H : C) (i : K ⟶ S.X₂) (π : K ⟶ H)
  (wi : CategoryTheory.CategoryStruct.comp i S.g = 0)
  (hi : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i wi))
  (wπ : CategoryTheory.CategoryStruct.comp (hi.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) π = 0)
  (hπ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π wπ)),
  sizeOf { K := K, H := H, i := i, π := π, wi := wi, hi := hi, wπ := wπ, hπ := hπ } =
    1 + sizeOf K + sizeOf H + sizeOf i + sizeOf π + sizeOf wi + sizeOf hi + sizeOf wπ + sizeOf hπ
-- Mathlib.Data.Set.Pairwise.Lattice
Set.coe_biUnionEqSigmaOfDisjoint_symm_apply : ∀ {α : Type u_5} {ι : Type u_6} {s : Set ι} {f : ι → Set α} (h : s.PairwiseDisjoint f) (x : (i : ↑s) × ↑(f ↑i)),
  ↑((Set.biUnionEqSigmaOfDisjoint h).symm x) = ↑x.snd
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.toEdge_preimage_singleton : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {u v : V} (h : M.IsMatching) (huv : M.Adj u v),
  h.toEdge ⁻¹' {⟨s(u, v), huv⟩} = {⟨u, ⋯⟩, ⟨v, ⋯⟩}
-- Mathlib.NumberTheory.Pell
/-- A solution with `x = 1` is trivial.  -/
Pell.Solution₁.eq_one_of_x_eq_one : ∀ {d : ℤ}, d ≠ 0 → ∀ {a : Pell.Solution₁ d}, a.x = 1 → a = 1
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.Iso.conj_eq_conj : ∀ {S : Type u} [inst : CommRing S] {X X' : ModuleCat S} (i : X ≅ X') (f : CategoryTheory.End X),
  i.conj f = { hom' := i.toLinearEquiv.conj (ModuleCat.Hom.hom f) }
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
cfc_im_id : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [inst_4 : StarModule ℂ A] [inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A),
  autoParam (IsStarNormal a) cfc_im_id._auto_1 → cfc (fun x => ↑x.im) a = ↑(imaginaryPart a)
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_20 : HAdd Std.Time.Minute.Offset Std.Time.Second.Offset Std.Time.Second.Offset
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_pow_X_add_C : ∀ {R : Type u} [inst : Semiring R] (r : R) (i : ℕ), ((Polynomial.X + Polynomial.C r) ^ i).leadingCoeff = 1
-- Mathlib.Topology.Algebra.Group.Pointwise
closure_subset_add_left_of_mem_nhds_zero_of_neg : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {s : Set G} (s' : Set G),
  s ∈ nhds 0 → (∀ x ∈ s, -x ∈ s) → closure s' ⊆ s + s'
-- Lean.Parser.Basic
Lean.Parser.noFirstTokenInfo : Lean.Parser.ParserInfo → Lean.Parser.ParserInfo
-- Mathlib.Logic.Equiv.Prod
/-- `PUnit` is a right identity for dependent type product up to an equivalence.  -/
Equiv.sigmaPUnit : (α : Type u_9) → (_ : α) × PUnit.{u_10 + 1} ≃ α
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Under.instHasLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.Limits.HasLimits C],
  CategoryTheory.Limits.HasLimits (CategoryTheory.Under X)
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.norm_completion : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  (f : NormedAddGroupHom G H), ‖f.completion‖ = ‖f‖
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.pow.match_1.eq_1 : ∀ (motive : Dyadic → Sort u_1) (h_1 : Unit → motive Dyadic.zero)
  (h_2 : (n k : ℤ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n k hn)),
  (match Dyadic.zero with
    | Dyadic.zero => h_1 ()
    | Dyadic.ofOdd n k hn => h_2 n k hn) =
    h_1 ()
-- Mathlib.RingTheory.Coalgebra.TensorProduct
Coalgebra.TensorProduct.lid_toLinearEquiv : ∀ {R : Type u_5} {P : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid P] [inst_2 : Module R P]
  [inst_3 : Coalgebra R P], (Coalgebra.TensorProduct.lid R P).toLinearEquiv = TensorProduct.lid R P
-- Std.Do.Triple.SpecLemmas
/-- Like `StringInvariant.withEarlyReturn`, but for the new `do` elaborator which uses `Prod`
instead of `MProd` for the state tuple.  -/
Std.Do.StringInvariant.withEarlyReturnNewDo : {β : Type (max u₁ u₂)} →
  {ps : Std.Do.PostShape} →
    {γ : Type (max u₁ u₂)} →
      {s : String} →
        (s.Pos → β → Std.Do.Assertion ps) →
          (γ → β → Std.Do.Assertion ps) →
            optParam (Std.Do.ExceptConds ps) Std.Do.ExceptConds.false → Std.Do.StringInvariant s (Option γ × β) ps
-- Mathlib.RingTheory.LaurentSeries
/-- The ring isomorphism between `K⟦X⟧` and the unit ball inside the `X`-adic completion of
`K⟮X⟯`.  -/
LaurentSeries.powerSeriesRingEquiv : (K : Type u_2) →
  [inst : Field K] →
    PowerSeries K ≃+* ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K))
-- Mathlib.Logic.Equiv.Defs
Equiv.psigmaCongrRight_refl : ∀ {α : Sort u_2} {β : α → Sort u_1}, (Equiv.psigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl ((a : α) ×' β a)
-- Mathlib.LinearAlgebra.Matrix.Ideal
Ideal.matrix_monotone : ∀ {R : Type u_1} [inst : Semiring R] (n : Type u_2) [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  Monotone (Ideal.matrix n)
-- Aesop.Tree.Data
Aesop.GoalData.mk : {Rapp MVarCluster : Type} →
  Aesop.GoalId →
    IO.Ref MVarCluster →
      Array (IO.Ref Rapp) →
        Aesop.GoalOrigin →
          ℕ →
            Aesop.GoalState →
              Bool →
                Bool →
                  Lean.MVarId →
                    Aesop.NormalizationState →
                      Aesop.UnorderedArraySet Lean.MVarId →
                        Aesop.ForwardState →
                          Aesop.ForwardRuleMatches →
                            Aesop.Percent →
                              Aesop.Iteration →
                                Aesop.Iteration →
                                  Bool → Aesop.UnsafeQueue → Array Aesop.RegularRule → Aesop.GoalData Rapp MVarCluster
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.BallPackage.mk.injEq : ∀ {β : Type u_1} {α : Type u_2} (c : β → α) (r : β → ℝ) (rpos : ∀ (b : β), 0 < r b) (r_bound : ℝ)
  (r_le : ∀ (b : β), r b ≤ r_bound) (c_1 : β → α) (r_1 : β → ℝ) (rpos_1 : ∀ (b : β), 0 < r_1 b) (r_bound_1 : ℝ)
  (r_le_1 : ∀ (b : β), r_1 b ≤ r_bound_1),
  ({ c := c, r := r, rpos := rpos, r_bound := r_bound, r_le := r_le } =
      { c := c_1, r := r_1, rpos := rpos_1, r_bound := r_bound_1, r_le := r_le_1 }) =
    (c = c_1 ∧ r = r_1 ∧ r_bound = r_bound_1)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `AddActionSemiHomClass F φ X Y` states that
`F` is a type of morphisms which are `φ`-equivariant.

You should extend this class when you extend `AddActionHom`.  -/
AddActionSemiHomClass : (F : Type u_8) →
  {M : outParam (Type u_9)} →
    {N : outParam (Type u_10)} →
      outParam (M → N) →
        (X : outParam (Type u_11)) → (Y : outParam (Type u_12)) → [VAdd M X] → [VAdd N Y] → [FunLike F X Y] → Prop
-- Lean.Meta.Tactic.FVarSubst
Lean.LocalDecl.applyFVarSubst : Lean.Meta.FVarSubst → Lean.LocalDecl → Lean.LocalDecl
-- Mathlib.Data.Fin.Tuple.Basic
Fin.eq_insertNth_iff : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} {a : α p} {f : (i : Fin n) → α (p.succAbove i)}
  {g : (j : Fin (n + 1)) → α j}, g = p.insertNth a f ↔ g p = a ∧ p.removeNth g = f
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- The reciprocal of the Gamma function is differentiable everywhere
(including the points where Gamma itself is not).  -/
Complex.differentiable_one_div_Gamma : Differentiable ℂ fun s => (Complex.Gamma s)⁻¹
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instIntCast : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [IntCast M] → IntCast (l.Germ M)