mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Max
/-- For each term `a`, there is some strictly greater `b`.  -/
NoMaxOrder.exists_gt : ∀ {α : Type u_3} {inst : LT α} [self : NoMaxOrder α] (a : α), ∃ b, a < b
-- Init.Data.Array.Attach
List.attachWith_toArray : ∀ {α : Type u_1} {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x},
  l.toArray.attachWith P H = (l.attachWith P ⋯).toArray
-- Init.Data.Range.Polymorphic.UInt
UInt8.instHasSize : Std.Rxc.HasSize UInt8
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ_σ₀Iter : ∀ (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : autoParam (n + i = m) SimplexCategory.σ_σ₀Iter._auto_1),
  autoParam (↑j ≤ i) SimplexCategory.σ_σ₀Iter._auto_3 →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (SimplexCategory.σ₀Iter i hi) =
      SimplexCategory.σ₀Iter (i + 1) ⋯
-- Mathlib.Order.Atoms
IsCoatom.le_iff : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] {a x : α}, IsCoatom a → (a ≤ x ↔ x = ⊤ ∨ x = a)
-- Mathlib.Combinatorics.Matroid.Basic
/-- The `aesop_mat` tactic attempts to prove a set is contained in the ground set of a matroid.
It uses a `[Matroid]` ruleset, and is allowed to fail.  -/
Matroid.aesop_mat : Lean.ParserDescr
-- Init.Grind.AC
Lean.Grind.AC.Seq.unionFuel.match_1.congr_eq_4 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (s₁ s₂ : Lean.Grind.AC.Seq)
  (h_1 : (x₁ x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.var x₂))
  (h_2 :
    (x₁ x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.cons x s))
  (h_3 :
    (x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) →
        (x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x₂))
  (h_4 :
    (x₁ : Lean.Grind.AC.Var) →
      (s₁ : Lean.Grind.AC.Seq) →
        (x₂ : Lean.Grind.AC.Var) →
          (s₂ : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x₁ s₁) (Lean.Grind.AC.Seq.cons x₂ s₂))
  (x₁ : Lean.Grind.AC.Var) (s₁_1 : Lean.Grind.AC.Seq) (x₂ : Lean.Grind.AC.Var) (s₂_1 : Lean.Grind.AC.Seq),
  s₁ = Lean.Grind.AC.Seq.cons x₁ s₁_1 →
    s₂ = Lean.Grind.AC.Seq.cons x₂ s₂_1 →
      (match s₁, s₂ with
        | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.var x₂ => h_1 x₁ x₂
        | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.cons x s => h_2 x₁ x s
        | Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x₂ => h_3 x s x₂
        | Lean.Grind.AC.Seq.cons x₁ s₁, Lean.Grind.AC.Seq.cons x₂ s₂ => h_4 x₁ s₁ x₂ s₂) ≍
        h_4 x₁ s₁_1 x₂ s₂_1
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.contDiffAt_rpow_const_of_le : ∀ {x p : ℝ} {n : ℕ}, ↑n ≤ p → ContDiffAt ℝ (↑n) (fun x => x ^ p) x
-- Mathlib.Topology.MetricSpace.Basic
/-- Build new metric space from an old one where the distance is provably (but typically
non-definitionally) equal to some given distance. We also provide convenience versions for
PseudoEMetric, PseudoMatric and EMetric spaces.  -/
MetricSpace.replaceDist : {X : Type u_2} → (m : MetricSpace X) → (d : X → X → ℝ) → d = dist → MetricSpace X
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.assoc_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d)
  [inst_1 :
    CategoryTheory.BicategoricalCoherence
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) i],
  CategoryTheory.BicategoricalCoherence.iso =
    CategoryTheory.Bicategory.associator f g h ≪≫ CategoryTheory.BicategoricalCoherence.iso
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesLimits'.newCone_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra}
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)),
  (CategoryTheory.Comonad.ForgetCreatesLimits'.newCone c).π =
    CategoryTheory.CategoryStruct.comp c.π CategoryTheory.Comonad.ForgetCreatesLimits'.γ
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.TriggerCondition.skip.sizeOf_spec : ∀ {ctx : Type u_1} [inst : SizeOf ctx], sizeOf Mathlib.TacticAnalysis.TriggerCondition.skip = 1
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_lt_div_iff_right : ∀ {a b c : ENNReal}, a ≠ 0 → a ≠ ⊤ → (a / b < a / c ↔ c < b)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_sup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) (P P' : CategoryTheory.MorphismProperty D),
  (P ⊔ P').inverseImage F = P.inverseImage F ⊔ P'.inverseImage F
-- Mathlib.CategoryTheory.Groupoid
/-- A category equipped with a fully faithful functor to a groupoid is fully faithful  -/
CategoryTheory.Groupoid.ofFullyFaithfulToGroupoid : {C : Type u_1} →
  [𝒞 : CategoryTheory.Category.{u_2, u_1} C] →
    {D : Type u} →
      [inst : CategoryTheory.Groupoid D] →
        (F : CategoryTheory.Functor C D) → F.FullyFaithful → CategoryTheory.Groupoid C
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.instSMulCommClassSubtypeMemCenter_1 : ∀ {M : Type u_2} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α], SMulCommClass M (↥(Submonoid.center M)) α
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.DTreeMap.minEntryD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → (a : α) × β a → (a : α) × β a
-- Mathlib.Algebra.Order.Archimedean.Basic
existsUnique_add_zsmul_mem_Ico : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G},
  0 < a → ∀ (b c : G), ∃! m, b + m • a ∈ Set.Ico c (c + a)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RioSliceData.range : {α : Type u} → {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RioSliceData α β → Std.Rio α
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.eta_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F),
  c.eta.inv.hom = CategoryTheory.CategoryStruct.id c.pt
-- Std.Async.UDP
/-- Receives data from an UDP socket. `size` is for the maximum bytes to receive.
The promise resolves when some data is available or an error occurs. If the socket
has not been previously bound with `bind`, it is automatically bound to `0.0.0.0`
(all interfaces) with a random port.
Furthermore calling this function in parallel with `recvSelector` is not supported.
 -/
Std.Async.UDP.Socket.recv : Std.Async.UDP.Socket → UInt64 → Std.Async.Async (ByteArray × Option Std.Net.SocketAddress)
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
/-- If `Γ` is arithmetic, its preimage in `SL(2, ℤ)` has finite index.  -/
Subgroup.IsArithmetic.finiteIndex_comap : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic], (Subgroup.comap (Matrix.SpecialLinearGroup.mapGL ℝ) 𝒢).FiniteIndex
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instDiv.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  LowerSet.instDiv = { div := fun s t => { carrier := Set.image2 (fun x1 x2 => x1 / x2) ↑s ↑t, lower' := ⋯ } }
-- Mathlib.Probability.Distributions.Fernique
/-- A quantity that appears in exponentials in the proof of Fernique's theorem.  -/
ProbabilityTheory.Fernique.logRatio : ENNReal → ℝ
-- Mathlib.Analysis.BoxIntegral.Basic
MeasureTheory.Measure.toBoxAdditive.congr_simp : ∀ {ι : Type u_1} [inst : Finite ι] (μ μ_1 : MeasureTheory.Measure (ι → ℝ)) (e_μ : μ = μ_1)
  [inst_1 : MeasureTheory.IsLocallyFiniteMeasure μ], μ.toBoxAdditive = μ_1.toBoxAdditive
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.unit_app_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (Y : D), e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.keysArray.eq_1 : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β),
  m.keysArray = Std.DHashMap.Raw.fold (fun acc k x => acc.push k) (Array.emptyWithCapacity m.size) m
-- Mathlib.Data.Set.Lattice
Set.biInter_le_eq_iInter : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {s : α → Set β}, ⋂ n, ⋂ m, ⋂ (_ : m ≤ n), s m = ⋂ n, s n
-- Init.Data.UInt.Lemmas
USize.toNat_ofNatLT : ∀ {n : ℕ} {h : n < USize.size}, (USize.ofNatLT n h).toNat = n
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
/-- **Alias** of the forward direction of `ContinuousLinearMapWOT.continuousAt_iff`. -/
ContinuousLinearMapWOT.continuousAt_inner_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {α : Type u_4} [inst_7 : TopologicalSpace α] {f : α → E →WOT[𝕜] F} {a : α},
  ContinuousAt f a → ∀ (x : E) (y : F), ContinuousAt (fun x_1 => inner 𝕜 y ((f x_1) x)) a
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.swapEquiv_unitIso_hom_app_hom_toFun : ∀ (X : TwoP) (a : ((CategoryTheory.Functor.id TwoP).obj X).toBipointed.X),
  (TwoP.swapEquiv.unitIso.hom.app X).hom.toFun a = a
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.mk.inj : ∀ {A : Type u_1} {σ : Type u_2} {inst : CommRing A} {inst_1 : SetLike σ A} {inst_2 : AddSubmonoidClass σ A} {𝒜 : ℕ → σ}
  {inst_3 : GradedRing 𝒜} {asHomogeneousIdeal : HomogeneousIdeal 𝒜} {isPrime : asHomogeneousIdeal.toIdeal.IsPrime}
  {not_irrelevant_le : ¬HomogeneousIdeal.irrelevant 𝒜 ≤ asHomogeneousIdeal} {asHomogeneousIdeal_1 : HomogeneousIdeal 𝒜}
  {isPrime_1 : asHomogeneousIdeal_1.toIdeal.IsPrime}
  {not_irrelevant_le_1 : ¬HomogeneousIdeal.irrelevant 𝒜 ≤ asHomogeneousIdeal_1},
  { asHomogeneousIdeal := asHomogeneousIdeal, isPrime := isPrime, not_irrelevant_le := not_irrelevant_le } =
      { asHomogeneousIdeal := asHomogeneousIdeal_1, isPrime := isPrime_1, not_irrelevant_le := not_irrelevant_le_1 } →
    asHomogeneousIdeal = asHomogeneousIdeal_1
-- Aesop.Search.Expansion
Aesop.RuleResult.failed : Aesop.RuleResult
-- Mathlib.Probability.Process.LocalProperty
_private.Mathlib.Probability.Process.LocalProperty.0.ProbabilityTheory.mkStrictMonoAux.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : SizeOf R] (f : Polynomial R) (monic_f : f.Monic) (g : Polynomial R)
  (cond : ∃ p₁ p₂ n, Polynomial.derivative f * p₁ + f * p₂ = g ^ n),
  sizeOf { f := f, monic_f := monic_f, g := g, cond := cond } = 1 + sizeOf f + sizeOf monic_f + sizeOf g + sizeOf cond
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerRight_left : ∀ {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] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) {G H : CategoryTheory.Functor C D}
  (α : G ⟶ H) (K : CategoryTheory.Functor D E),
  CategoryTheory.Functor.whiskerRight (F.whiskerLeft α) K =
    CategoryTheory.CategoryStruct.comp (F.associator G K).hom
      (CategoryTheory.CategoryStruct.comp (F.whiskerLeft (CategoryTheory.Functor.whiskerRight α K))
        (F.associator H K).inv)
-- Mathlib.Algebra.Group.Defs
neg_add_cancel_right : ∀ {G : Type u_1} [inst : AddGroup G] (a b : G), a + -b + b = a
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.borelLower_eq : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [inst_4 : Fintype ι] [IsDomain R]
  [CharZero R] [Module.IsTorsionFree R L],
  b.borelLower = ⨆ n, ⨆ (_ : n ≠ 0), LieAlgebra.rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.stieltjesOfMeasurableRat.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → ℚ → ℝ) (hf : Measurable f),
  ProbabilityTheory.stieltjesOfMeasurableRat f hf = ⋯.stieltjesFunction
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.instIsStableUnderRetractsOfIsClosedUnderColimitsOfShapeWalkingParallelPair : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderColimitsOfShape CategoryTheory.Limits.WalkingParallelPair], P.IsStableUnderRetracts
-- Mathlib.Probability.Density
/-- If `X` is a random variable, then `pdf X ℙ μ`
is the Radon–Nikodym derivative of the push-forward measure of `ℙ` along `X` with respect to `μ`.  -/
MeasureTheory.pdf : {Ω : Type u_1} →
  {E : Type u_2} →
    [inst : MeasurableSpace E] →
      {x : MeasurableSpace Ω} →
        (Ω → E) → MeasureTheory.Measure Ω → autoParam (MeasureTheory.Measure E) MeasureTheory.pdf._auto_1 → E → ENNReal
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.mk : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c},
  (∀ (i₁ : ι₁) (i₂ : ι₂), e₁.f i₁ ≠ e₂.f i₂) →
    (∀ (i : ι), (∃ i₁, e₁.f i₁ = i) ∨ ∃ i₂, e₂.f i₂ = i) → e₁.AreComplementary e₂
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.instInhabited : (α : Type u_2) → [inst : Preorder α] → Inhabited (PseudoEpimorphism α α)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The center is commutative and associative.  -/
NonUnitalSubring.center.instNonUnitalCommRing : (R : Type u) → [inst : NonUnitalNonAssocRing R] → NonUnitalCommRing ↥(NonUnitalSubring.center R)
-- Mathlib.RingTheory.LocalRing.Pullback
AlgHom.isLocalRing_pullback : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Ring A]
  [inst_2 : Algebra R A] [inst_3 : Ring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  [IsLocalRing A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) [IsLocalHom g], IsLocalRing ↥(f.pullback g)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_eq_some_getKey!_of_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α}, m.contains a = true → m.getKey? a = some (m.getKey! a)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_le_size_alter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, m.size - 1 ≤ (m.alter k f).size
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_mul_inl : ∀ {R : Type u} (M : Type v) [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] (r₁ r₂ : R),
  TrivSqZeroExt.inl r₁ * TrivSqZeroExt.inl r₂ = TrivSqZeroExt.inl (r₁ * r₂)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Raw.Const.modify t k f).getKey? k = if k ∈ t then some k else none
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.types_congr_hom : ∀ {X Y : Type u} {f g : X ⟶ Y},
  f = g → ∀ (x : X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.instCategory.eq_1 : AddMagmaCat.instCategory =
  { Hom := fun X Y => X.Hom Y, id := fun X => { hom' := AddHom.id ↑X },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @AddMagmaCat.instCategory._proof_1,
    comp_id := @AddMagmaCat.instCategory._proof_2, assoc := @AddMagmaCat.instCategory._proof_3 }
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
AddMonoidHom.codRestrict.congr_simp : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {S : Type u_5} [inst_2 : SetLike S N]
  [inst_3 : AddSubmonoidClass S N] (f f_1 : M →+ N) (e_f : f = f_1) (s : S) (h : ∀ (x : M), f x ∈ s),
  f.codRestrict s h = f_1.codRestrict s ⋯
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Real.diam_Ioc : ∀ {a b : ℝ}, a ≤ b → Metric.diam (Set.Ioc a b) = b - a
-- Mathlib.CategoryTheory.Subobject.Basic
/-- We can map subobjects of `X` to subobjects of `Y`
by post-composition with a monomorphism `f : X ⟶ Y`.
 -/
CategoryTheory.Subobject.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [CategoryTheory.Mono f] → CategoryTheory.Functor (CategoryTheory.Subobject X) (CategoryTheory.Subobject Y)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
map_multiset_ne_zero_sum : ∀ {F : Type u_1} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : FunLike F M N] [AddHomClass F M N] (f : F) {s : Multiset M}, s ≠ 0 → f s.sum = (Multiset.map (⇑f) s).sum
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.IsSupportedOutside.mk : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : HomologicalComplex C c'} {e : c.Embedding c'}, (∀ (i : ι), K.ExactAt (e.f i)) → K.IsSupportedOutside e
-- Mathlib.CategoryTheory.Preadditive.Schur
/-- The part of **Schur's lemma** that holds in any preadditive category with kernels:
that a nonzero morphism between simple objects is an isomorphism.
 -/
CategoryTheory.isIso_of_hom_simple : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasKernels C] {X Y : C} [CategoryTheory.Simple X] [CategoryTheory.Simple Y] {f : X ⟶ Y},
  f ≠ 0 → CategoryTheory.IsIso f
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.instSplitEpiCategory : CategoryTheory.SplitEpiCategory SimplexCategory
-- Mathlib.Tactic.Rify
Mathlib.Tactic.Rify.ofNat_rat_real : ∀ (a : ℕ) [inst : a.AtLeastTwo], ↑(OfNat.ofNat a) = OfNat.ofNat a
-- Mathlib.Computability.TuringMachine.Computable
/-- the program itself, i.e. one function for every function label  -/
Turing.FinTM2.m : (self : Turing.FinTM2) → self.Λ → Turing.TM2.Stmt self.Γ self.Λ self.σ
-- Lean.Elab.Tactic.Grind.Param
/-- Helper method for processing parameters in tactics such as `finish` and `finish?`
 -/
Lean.Elab.Tactic.Grind.withParams : {α : Type} →
  Lean.Meta.Grind.Params →
    Lean.TSyntaxArray `Lean.Parser.Tactic.grindParam →
      Bool → Lean.Elab.Tactic.Grind.GrindTacticM α → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Mathlib.Tactic.Explode.Datatypes
/-- Add the entry unless it already exists. Sets the `line` field to the next
available value.  -/
Mathlib.Explode.Entries.add : Mathlib.Explode.Entries → Lean.Expr → Mathlib.Explode.Entry → Mathlib.Explode.Entry × Mathlib.Explode.Entries
-- Mathlib.MeasureTheory.Group.Action
/-- See also `smul_ae`.  -/
MeasureTheory.tendsto_smul_ae : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : SMul G α] (μ : MeasureTheory.Measure α)
  [MeasureTheory.SMulInvariantMeasure G α μ] (c : G),
  Filter.Tendsto (fun x => c • x) (MeasureTheory.ae μ) (MeasureTheory.ae μ)
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Get the norm rules corresponding to the norm rule matches.  -/
Aesop.ForwardRuleMatches.normRules : Aesop.ForwardRuleMatches → Array Aesop.NormRule
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
/-- The map of a binary cofan is a colimit iff
the cofork consisting of the mapped morphisms is a colimit.
This essentially lets us commute `BinaryCofan.mk` with `Functor.mapCocone`.
 -/
CategoryTheory.Limits.isColimitMapCoconeBinaryCofanEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {P X Y : C} →
            (f : X ⟶ P) →
              (g : Y ⟶ P) →
                CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.BinaryCofan.mk f g)) ≃
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (G.map f) (G.map g))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {f : α → β → Bool} {k : α},
  (Std.TreeMap.filter f t)[k]! = (t[k]?.pfilter fun x h' => f (t.getKey k ⋯) x).get!
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_insert_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  t.isEmpty = true → (t.insert k).min! = k
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubAddAction.fg_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : VAdd R M] {p : SubAddAction R M}, p.FG ↔ ∃ s, p = SubAddAction.closure R ↑s
-- Std.Http.Data.URI.Basic
Std.Http.URI.Path.mk.inj : ∀ {segments : Array Std.Http.URI.EncodedSegment} {absolute : Bool} {segments_1 : Array Std.Http.URI.EncodedSegment}
  {absolute_1 : Bool},
  { segments := segments, absolute := absolute } = { segments := segments_1, absolute := absolute_1 } →
    segments = segments_1 ∧ absolute = absolute_1
-- Mathlib.Topology.Constructible
_private.Mathlib.Topology.Constructible.0.Topology.infClosed_isLocallyConstructible : ∀ {X : Type u_2} [inst : TopologicalSpace X], InfClosed {s | Topology.IsLocallyConstructible s}
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ici_ne_Ici : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, UpperSet.Ici a ≠ UpperSet.Ici b ↔ a ≠ b
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
/-- If an initial object `I` exists in a CCC, then `A ⨯ I ≅ I`.  -/
CategoryTheory.zeroMul : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {A : C} →
        [CategoryTheory.Closed A] →
          {I : C} → CategoryTheory.Limits.IsInitial I → (CategoryTheory.MonoidalCategoryStruct.tensorObj A I ≅ I)
-- Mathlib.Data.Stream.Init
Stream'.get_of_bisim : ∀ {α : Type u} (R : Stream' α → Stream' α → Prop),
  Stream'.IsBisimulation R →
    ∀ {s₁ s₂ : Stream' α} (n : ℕ), R s₁ s₂ → s₁.get n = s₂.get n ∧ R (Stream'.drop (n + 1) s₁) (Stream'.drop (n + 1) s₂)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.IsLimit.homIso_apply_coe : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {t : CategoryTheory.Limits.Trident f} (ht : CategoryTheory.Limits.IsLimit t) (Z : C) (k : Z ⟶ t.pt),
  ↑((CategoryTheory.Limits.Trident.IsLimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp k t.ι
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.subtype_injective : ∀ {K : Type u} [inst : Field K] (R : ValuationSubring K), Function.Injective ⇑R.subtype
-- Mathlib.Analysis.InnerProductSpace.Positive
_private.Mathlib.Analysis.InnerProductSpace.Positive.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Data.ZMod.Basic
zmod_val_inv_nsmul_nsmul : ∀ {α : Type u_1} [inst : AddGroup α] {n : ℕ}, (Nat.card α).gcd n = 1 → ∀ (a : α), (↑n)⁻¹.val • n • a = a
-- Mathlib.CategoryTheory.Comma.Over.OverClass
/-- The structure morphism `X ↘ S : X ⟶ S` given `OverClass X S`.  -/
CategoryTheory.«term_↘_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.sub_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂), (φ - φ').τ₃ = φ.τ₃ - φ'.τ₃
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vaddFinset.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β],
  Finset.vaddFinset = { vadd := fun a => Finset.image fun x => a +ᵥ x }