mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
/-- Constructor for oplax functors from a locally discrete bicategory. In that
case, we do not need to provide the `map₂` field of oplax functors.  -/
CategoryTheory.oplaxFunctorOfIsLocallyDiscrete : {B : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Bicategory B] →
      [inst_1 : CategoryTheory.Bicategory.IsLocallyDiscrete B] →
        [inst_2 : CategoryTheory.Bicategory C] →
          (obj : B → C) →
            (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) →
              (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b)) →
                (mapComp :
                    {b₀ b₁ b₂ : B} →
                      (f : b₀ ⟶ b₁) →
                        (g : b₁ ⟶ b₂) →
                          map (CategoryTheory.CategoryStruct.comp f g) ⟶
                            CategoryTheory.CategoryStruct.comp (map f) (map g)) →
                  autoParam
                      (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
                            (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h))
                              (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) =
                          CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h)
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h))
                              (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom))
                      CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_1 →
                    autoParam
                        (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
                          CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f)
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f))
                                (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
                            CategoryTheory.eqToHom ⋯)
                        CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_3 →
                      autoParam
                          (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
                            CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁))
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁))
                                  (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
                              CategoryTheory.eqToHom ⋯)
                          CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_5 →
                        CategoryTheory.OplaxFunctor B C
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_snd : ∀ {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : CategoryTheory.Limits.PullbackCone f g}
  (hc : CategoryTheory.Limits.IsLimit c) (x : c.pt),
  (↑((CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj hc) x)).2 =
    (CategoryTheory.ConcreteCategory.hom c.snd) x
-- Mathlib.MeasureTheory.Measure.MeasuredSets
MeasureTheory.MeasuredSets.dist_def : ∀ {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
  (s t : MeasureTheory.MeasuredSets μ), dist s t = μ.real (symmDiff ↑s ↑t)
-- Lean.Server.References
Lean.Server.References.mk.injEq : ∀ (ileans : Lean.Server.ILeanMap) (workers : Lean.Server.WorkerRefMap) (ileans_1 : Lean.Server.ILeanMap)
  (workers_1 : Lean.Server.WorkerRefMap),
  ({ ileans := ileans, workers := workers } = { ileans := ileans_1, workers := workers_1 }) =
    (ileans = ileans_1 ∧ workers = workers_1)
-- Init.Data.Vector.FinRange
Vector.finRange_reverse : ∀ {n : ℕ}, (Vector.finRange n).reverse = Vector.map Fin.rev (Vector.finRange n)
-- Mathlib.RingTheory.Localization.AtPrime.Extension
IsLocalization.AtPrime.liesOver_map_of_liesOver : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Rₚ : Type u_3) [inst_4 : CommRing Rₚ] [inst_5 : Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p]
  [inst_7 : IsLocalRing Rₚ] (Sₚ : Type u_4) [inst_8 : CommRing Sₚ] [inst_9 : Algebra S Sₚ]
  [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [inst_11 : Algebra Rₚ Sₚ] (P : Ideal S)
  [hPp : P.LiesOver p] [inst_12 : Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] [P.IsPrime],
  (Ideal.map (algebraMap S Sₚ) P).LiesOver (IsLocalRing.maximalIdeal Rₚ)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.Integrable.indicator₀ : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] {f : α → ε'},
  MeasureTheory.Integrable f μ → MeasureTheory.NullMeasurableSet s μ → MeasureTheory.Integrable (s.indicator f) μ
-- Mathlib.Algebra.Algebra.Hom
AlgHom.mk : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                (toRingHom : A →+* B) →
                  (∀ (r : R), (↑↑toRingHom).toFun ((algebraMap R A) r) = (algebraMap R B) r) → A →ₐ[R] B
-- Mathlib.Data.ZMod.Aut
ZMod.AddAutEquivUnits_apply : ∀ (n : ℕ) (f : AddAut (ZMod n)), (ZMod.AddAutEquivUnits n) f = Additive.ofMul (Units.mkOfMulEqOne (f 1) ((-f) 1) ⋯)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.State.mk.inj : ∀ {α : Type} {values : Std.Queue α} {consumers : Std.Queue (Std.CloseableChannel.Consumer✝ α)} {closed : Bool}
  {values_1 : Std.Queue α} {consumers_1 : Std.Queue (Std.CloseableChannel.Consumer✝ α)} {closed_1 : Bool},
  { values := values, consumers := consumers, closed := closed } =
      { values := values_1, consumers := consumers_1, closed := closed_1 } →
    values = values_1 ∧ consumers = consumers_1 ∧ closed = closed_1
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.lift_neg_right_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj B] (f g h : A ⟶ B),
  CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CartesianMonoidalCategory.lift f
          (CategoryTheory.CategoryStruct.comp g CategoryTheory.AddGrpObj.neg))
        CategoryTheory.AddMonObj.add =
      h ↔
    f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift h g)
        CategoryTheory.AddMonObj.add
-- Mathlib.Topology.Connected.PathConnected
PathConnectedSpace.instSubsingletonZerothHomotopy : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PathConnectedSpace X], Subsingleton (ZerothHomotopy X)
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.single.congr_simp : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → Zero (M i)] {inst_1 : DecidableEq ι} [inst_2 : DecidableEq ι]
  (i : ι) (x x_1 : M i), x = x_1 → ∀ (j : ι), Pi.single i x j = Pi.single i x_1 j
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.SameKeys.balanced : ∀ {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Std.DTreeMap.Internal.Impl α β}
  {t' : Std.DTreeMap.Internal.Impl α β'}, t.SameKeys t' → t.Balanced → t'.Balanced
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNorm.mk.injEq : ∀ {R : Type u_1} [inst : SeminormedCommRing R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S]
  (toMulRingNorm : MulRingNorm S) (smul' : ∀ (a : R) (x : S), toMulRingNorm.toFun (a • x) = ‖a‖ * toMulRingNorm.toFun x)
  (toMulRingNorm_1 : MulRingNorm S)
  (smul'_1 : ∀ (a : R) (x : S), toMulRingNorm_1.toFun (a • x) = ‖a‖ * toMulRingNorm_1.toFun x),
  ({ toMulRingNorm := toMulRingNorm, smul' := smul' } = { toMulRingNorm := toMulRingNorm_1, smul' := smul'_1 }) =
    (toMulRingNorm = toMulRingNorm_1)
-- Mathlib.RingTheory.Ideal.Basic
/-- A bijection between (left) ideals of a division ring and `{0, 1}`, sending `⊥` to `0`
and `⊤` to `1`.  -/
Ideal.equivFinTwo : (K : Type u_5) → [inst : DivisionSemiring K] → Ideal K ≃ Fin 2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k : α}
  {v : β},
  t.WF →
    (Std.DTreeMap.Internal.Impl.Const.get? t k = some v ↔
      ∃ k', compare k k' = Ordering.eq ∧ (k', v) ∈ Std.DTreeMap.Internal.Impl.Const.toArray t)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_eq_some_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k : α} {v : β},
      Std.DHashMap.Internal.Raw₀.Const.get? m k = some v ↔
        ∃ (h : m.contains k = true), Std.DHashMap.Internal.Raw₀.Const.get m k h = v
-- Mathlib.Topology.Algebra.ProperConstSMul
instProperConstSMulOfContinuousConstSMul : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace X]
  [ContinuousConstSMul G X], ProperConstSMul G X
-- Mathlib.Data.BitVec
BitVec.toFin_intCast : ∀ {w : ℕ} (z : ℤ), (↑z).toFin = ↑z
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combine_k_eq_combine : ∀ (p₁ p₂ : Lean.Grind.CommRing.Poly), p₁.combine_k p₂ = p₁.combine p₂
-- Mathlib.NumberTheory.LSeries.Deriv
/-- The abscissa of absolute convergence of the point-wise product of a power of `log` and `f`
is the same as that of `f`.  -/
LSeries.absicssaOfAbsConv_logPowMul : ∀ {f : ℕ → ℂ} {m : ℕ}, LSeries.abscissaOfAbsConv (LSeries.logMul^[m] f) = LSeries.abscissaOfAbsConv f
-- Mathlib.Order.TransfiniteIteration
/-- The `j`th-iteration of a function `φ : I → I` when `j : J` belongs to
a well-ordered type.  -/
transfiniteIterate : {I : Type u} →
  [SupSet I] → (I → I) → {J : Type w} → [inst : LinearOrder J] → [SuccOrder J] → [WellFoundedLT J] → J → I → I
-- Lean.Meta.Tactic.TryThis
/-- Evaluates `tac` in `initialState` without recovery or sorrying on elaboration failure. If
`expectedType?` is non-`none`, an error is thrown if the resulting goal type is not equal to the
provided type (up to `Expr` equality modulo metavariable instantiation).
 -/
_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.evalTacticWithState : Lean.Elab.Tactic.SavedState → Lean.TSyntax `tactic → optParam (Option Lean.Expr) none → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Data.Rat.Defs
Rat.coe_int_num_of_den_eq_one : ∀ {q : ℚ}, q.den = 1 → ↑q.num = q
-- Mathlib.Algebra.Group.Subgroup.Finsupp
AddSubgroup.exists_finsupp_of_mem_closure_range : ∀ {M : Type u_1} [inst : AddCommGroup M] {ι : Type u_2} (f : ι → M),
  ∀ x ∈ AddSubgroup.closure (Set.range f), ∃ a, x = a.sum fun x1 x2 => x2 • f x1
-- Mathlib.RingTheory.LocalProperties.Semilocal
/-- A module `M` over a semilocal ring `R` is finite if
its localization at every maximal ideal is finite.  -/
Module.Finite.of_isLocalized_maximal : ∀ {R : Type u_1} [inst : CommSemiring R] [Finite (MaximalSpectrum R)] (M : Type u_2) [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3)
  [inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)]
  [inst_5 : (P : Ideal R) → [inst_5 : P.IsMaximal] → Algebra R (Rₚ P)]
  [∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4) [inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_8 : (P : Ideal R) → [inst_8 : P.IsMaximal] → Module R (Mₚ P)]
  [inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)]
  [∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)]
  (f : (P : Ideal R) → [inst_11 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)],
  (∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)) → Module.Finite R M
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPoly.beq_spec_1 : ∀ (a b : ℤ), (Lean.Grind.CommRing.Poly.num a == Lean.Grind.CommRing.Poly.num b) = (a == b)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult.term : Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult → Lean.Syntax
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHSubOffset_6 : HSub Std.Time.WallTime Std.Time.Nanosecond.Offset Std.Time.WallTime
-- Mathlib.Algebra.Homology.ComplexShape
/-- The `ComplexShape` allowing differentials from `X i` to `X (i+a)`.
(For example when `a = 1`, a cohomology theory indexed by `ℕ` or `ℤ`)
 -/
ComplexShape.up' : {α : Type u_2} → [inst : Add α] → [IsRightCancelAdd α] → α → ComplexShape α
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instNonUnitalNonAssocSemiring : {R : Type u_1} → [NonUnitalNonAssocSemiring R] → NonUnitalNonAssocSemiring Rᵐᵒᵖ
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.exists_one_add_mul_pow_prime_pow_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} {u v : R},
  Nat.Prime p → v ∣ u → ↑p * u * v ∣ u ^ p → ∀ (x : R) (m : ℕ), ∃ y, (1 + u * x) ^ p ^ m = 1 + ↑p ^ m * u * (x + v * y)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.bounded : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β]
  [inst_3 : FunLike F α β] [ZeroAtInftyContinuousMapClass F α β] (f : F), ∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C
-- Mathlib.Order.Hom.Basic
/-- `OrderIsoClass F α β` states that `F` is a type of order isomorphisms.

You should extend this class when you extend `OrderIso`.  -/
OrderIsoClass : (F : Type u_6) → (α : outParam (Type u_7)) → (β : outParam (Type u_8)) → [LE α] → [LE β] → [EquivLike F α β] → Prop
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.Hom.w_assoc : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g) {Z : T}
  (h : g.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) (CategoryTheory.CategoryStruct.comp g.hom h) =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right sq) h)
-- Mathlib.Analysis.RCLike.Basic
RCLike.nnnorm_natCast : ∀ {K : Type u_1} [inst : RCLike K] (n : ℕ), ‖↑n‖₊ = ↑n
-- Init.System.IO
EIO.adapt : {ε ε' α : Type} → (ε → ε') → EIO ε α → EIO ε' α
-- Mathlib.NumberTheory.AbelSummation
/-- A version of `summable_mul_of_bigO_atTop` that can be useful to avoid difficulties near zero.  -/
summable_mul_of_bigO_atTop' : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜},
  (∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖f x‖) t) →
    MeasureTheory.LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 1) MeasureTheory.volume →
      ((fun n => ‖f ↑n‖ * ∑ k ∈ Finset.Icc 1 n, ‖c k‖) =O[Filter.atTop] fun x => 1) →
        ∀ {g : ℝ → ℝ},
          (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Finset.Icc 1 ⌊t⌋₊, ‖c k‖) =O[Filter.atTop] g →
            MeasureTheory.IntegrableAtFilter g Filter.atTop MeasureTheory.volume → Summable fun n => f ↑n * c n
-- Mathlib.Algebra.GCDMonoid.Basic
Associated.lcm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a₁ a₂ b₁ b₂ : α},
  Associated a₁ a₂ → Associated b₁ b₂ → Associated (lcm a₁ b₁) (lcm a₂ b₂)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.eq_ones_iff : ∀ {n : ℕ} {c : Composition n}, c = Composition.ones n ↔ ∀ i ∈ c.blocks, i = 1
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.isEmpty_empty : IsEmpty FirstOrder.Language.empty.Symbols
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.LawfulMapOperator.instMkNotCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.RefVec.LawfulMapOperator α Std.Sat.AIG.mkNotCached
-- Mathlib.Analysis.Complex.Angle
Complex.angle_mul_left : ∀ {a : ℂ}, a ≠ 0 → ∀ (x y : ℂ), InnerProductGeometry.angle (a * x) (a * y) = InnerProductGeometry.angle x y
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeffAddEquiv_apply`. -/
SkewMonoidAlgebra.toFinsuppAddEquiv_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (self : SkewMonoidAlgebra k G),
  SkewMonoidAlgebra.coeffAddEquiv self = self.coeff
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.of_mulEquivOfMulEquiv_apply : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {T : Submonoid P} {Q : Type u_4} [inst_3 : CommMonoid Q]
  {k : T.LocalizationMap Q} {j : M ≃* P} (H : Submonoid.map j.toMonoidHom S = T) (x : M),
  (f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H)) x = k (j x)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X}
  (c : CategoryTheory.Limits.PullbackCone f g),
  CategoryTheory.Limits.pullbackConeEquivBinaryFan.functor.obj c =
    CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Over.homMk c.fst ⋯) (CategoryTheory.Over.homMk c.snd ⋯)
-- Mathlib.Topology.Category.TopCat.Sphere
TopCat.instMonoDiskBoundaryInclusion : ∀ {n : ℕ}, CategoryTheory.Mono (TopCat.diskBoundaryInclusion n)
-- Mathlib.Logic.Basic
Fact.elim : ∀ {p : Prop}, Fact p → p
-- Mathlib.FieldTheory.Separable
/-- Typeclass for separable field extension: `K` is a separable field extension of `F` iff
the minimal polynomial of every `x : K` is separable. This implies that `K/F` is an algebraic
extension, because the minimal polynomial of a non-integral element is `0`, which is not
separable.

We define this for general (commutative) rings and only assume `F` and `K` are fields if this
is needed for a proof.  -/
Algebra.IsSeparable : (F : Type u_1) → (K : Type u_3) → [inst : CommRing F] → [inst_1 : Ring K] → [Algebra F K] → Prop
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_def : ∀ {R : Type u_3} [inst : Semiring R] (p : Polynomial R) {S : Type u_4} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
  [inst_3 : MulActionWithZero R S] (x : S), p.smeval x = p.sum (Polynomial.smul_pow x)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.preservesZeroMorphisms_π₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  CategoryTheory.ShortComplex.π₂.PreservesZeroMorphisms
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.isoClosure_strictMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D), (P.strictMap F).isoClosure = P.map F
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [inst : TopologicalSpace β]
  [inst_1 : TopologicalSpace γ] {f : α → β × γ},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => (f x).2
-- Mathlib.Data.Num.Basic
/-- Multiplication of two `PosNum`s.  -/
PosNum.mul : PosNum → PosNum → PosNum
-- Mathlib.Algebra.Notation.Lemmas
one_le_ite : ∀ {α : Type u_1} [inst : One α] {p : Prop} [inst_1 : Decidable p] {a b : α} [inst_2 : LE α],
  1 ≤ a → 1 ≤ b → 1 ≤ if p then a else b
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
AnalyticOnNhd.iteratedFDeriv_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E}, AnalyticOnNhd 𝕜 f s → IsOpen s → ∀ (n : ℕ), AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter.unique : ∀ (L : Type u) [inst : CommRing L] [inst_1 : IsDomain L] {n : ℕ} [inst_2 : NeZero n]
  (hn : Nat.card ↥(rootsOfUnity n L) = n) (g : L ≃+* L) {c : ZMod n},
  (∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val) → c = ↑((modularCyclotomicCharacter L hn) g)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.return.sizeOf_spec : ∀ (ref val : Lean.Syntax), sizeOf (Lean.Elab.Term.Do.Code.return ref val) = 1 + sizeOf ref + sizeOf val
-- Mathlib.Topology.Semicontinuity.Defs
hasOpenLowerSections_iff_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β},
  HasOpenLowerSections f ↔ ∀ (b : β), IsOpen {x | b ∈ f x}
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.le_le_combine : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α] [Lean.Grind.OrderedAdd α]
  (ctx : Lean.Grind.Linarith.Context α) (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.le_le_combine_cert p₁ p₂ p₃ = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ ≤ 0 →
      Lean.Grind.Linarith.Poly.denote' ctx p₂ ≤ 0 → Lean.Grind.Linarith.Poly.denote' ctx p₃ ≤ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The morphism to the zero object determines a cocone on a cokernel diagram  -/
CategoryTheory.Limits.cokernel.zeroCokernelCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasZeroObject C] → CategoryTheory.Limits.CokernelCofork f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option β → Option β},
  m.WF →
    (m.alter k f).size =
      if k ∈ m ∧ (f m[k]?).isNone = true then m.size - 1
      else if k ∉ m ∧ (f m[k]?).isSome = true then m.size + 1 else m.size
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.toContinuousLinearMap_symm_ridIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ↑↑(TensorProduct.ridIsometry 𝕜 E).symm = (TensorProduct.mkL 𝕜 E 𝕜).flip 1
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertDateTime : Std.Time.DateTime → optParam Bool false → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Topology.MetricSpace.Gluing
Metric.dense_iUnion_range_toInductiveLimit : ∀ {X : ℕ → Type u} [inst : (n : ℕ) → MetricSpace (X n)] {f : (n : ℕ) → X n → X (n + 1)} (I : ∀ (n : ℕ), Isometry (f n)),
  Dense (⋃ i, Set.range (Metric.toInductiveLimit I i))
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.FunctorsInverting.comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {W : CategoryTheory.MorphismProperty C} {F₁ F₂ F₃ : W.FunctorsInverting D} (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inl_snd_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.Calculus.DiffContOnCl
DifferentiableOn.diffContOnCl_ball : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {U : Set E} {c : E}
  {R : ℝ}, DifferentiableOn 𝕜 f U → Metric.closedBall c R ⊆ U → DiffContOnCl 𝕜 f (Metric.ball c R)