mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The scalar multiplication of a constant and a `C^n` function on a domain is `C^n`.  -/
ContDiffOn.const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {R : Type u_3} [inst_5 : DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {s : Set E} {f : E → F}
  (c : R), ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n (fun y => c • f y) s
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f}
  {hom : (i : ι) → D₁.obj i ⟶ D₂.obj i}
  {comm :
    autoParam
      (∀ (i₁ i₂ : ι),
        CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom i₂))) =
          CategoryTheory.CategoryStruct.comp (hom i₁) (D₂.hom i₁ i₂))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.comm._autoParam}
  {hom_1 : (i : ι) → D₁.obj i ⟶ D₂.obj i}
  {comm_1 :
    autoParam
      (∀ (i₁ i₂ : ι),
        CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom_1 i₂))) =
          CategoryTheory.CategoryStruct.comp (hom_1 i₁) (D₂.hom i₁ i₂))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.comm._autoParam},
  { hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 } → hom = hom_1
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableAt.comp_mdifferentiableWithinAt_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {s : Set M} {g : M' → M''} {y : M'},
  MDiffAt g y → MDiffAt[s] f x → f x = y → MDiffAt[s] (g ∘ f) x
-- Init.Data.Fin.Lemmas
Fin.ofNat_val_eq_self : ∀ {n : ℕ} [inst : NeZero n] (x : Fin n), Fin.ofNat n ↑x = x
-- Mathlib.Algebra.Order.Kleene
le_kstar : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a : α}, a ≤ KStar.kstar a
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.glue_eq_glue! : ∀ {α : Type u} {β : α → Type v} {l r : Std.DTreeMap.Internal.Impl α β} {hl : l.Balanced} {hr : r.Balanced}
  {hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size}, l.glue r hl hr hlr = l.glue! r
-- Mathlib.Data.List.Rotate
List.rotate_perm : ∀ {α : Type u} (l : List α) (n : ℕ), (l.rotate n).Perm l
-- Init.Data.Nat.Basic
Nat.rec_eq_recCompiled : @Nat.rec = @Nat.recCompiled
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
/-- The `lintegral` transforms appropriately under a measurable equivalence `g : α ≃ᵐ β`.
(Compare `lintegral_map`, which applies to a wider class of functions `g : α → β`, but requires
measurability of the function being integrated.)  -/
MeasureTheory.lintegral_map_equiv : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  (f : β → ENNReal) (g : α ≃ᵐ β), ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map (⇑g) μ = ∫⁻ (a : α), f (g a) ∂μ
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_eq_one : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] {a : α}, a⁺ᵐ = 1 ↔ a ≤ 1
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- If the `d`th coefficient of a formal power series is nonzero,
then the order of the power series is less than or equal to `degree d`.  -/
MvPowerSeries.order_le : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R} {d : σ →₀ ℕ},
  (MvPowerSeries.coeff d) f ≠ 0 → f.order ≤ ↑(Finsupp.degree d)
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  LeftOrdContinuous f → RightOrdContinuous (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
-- Mathlib.Tactic.Generalize
/-- Backwards compatibility shim for `generalize`.  -/
«tacticGeneralize'_:_=_» : Lean.ParserDescr
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
_private.Mathlib.RingTheory.MvPolynomial.Homogeneous.0.MvPolynomial.IsHomogeneous.exists_eval_ne_zero_of_coeff_finSuccEquiv_ne_zero_aux : ∀ {R : Type u_3} [inst : CommSemiring R] {N : ℕ} {F : MvPolynomial (Fin N.succ) R} {n : ℕ},
  F.IsHomogeneous n → ((MvPolynomial.finSuccEquiv R N) F).coeff n ≠ 0 → ∃ r, (MvPolynomial.eval r) F ≠ 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m₁ \ m₂).contains k = (m₁.contains k && !m₂.contains k)
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A constant to which a Cauchy filter in a discrete uniform space converges.  -/
DiscreteUniformity.cauchyConst : {α : Type u} → [uniformSpace : UniformSpace α] → [DiscreteUniformity α] → {f : Filter α} → Cauchy f → α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- **Alias** of the reverse direction of `Real.sinh_pos_iff`. -/
Mathlib.Meta.Positivity.sinh_pos_of_pos : ∀ {x : ℝ}, 0 < x → 0 < Real.sinh x
-- Mathlib.Topology.DiscreteSubset
mem_codiscrete' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set X}, S ∈ Filter.codiscrete X ↔ IsOpen S ∧ IsDiscrete Sᶜ
-- Mathlib.Topology.MetricSpace.Thickening
/-- **Alias** of `Metric.infEDist_le_infEDist_cthickening_add`.

---

For the equality, see `infEDist_cthickening`.  -/
Metric.infEdist_le_infEdist_cthickening_add : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {s : Set α} {x : α},
  Metric.infEDist x s ≤ Metric.infEDist x (Metric.cthickening δ s) + ENNReal.ofReal δ
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- If `F` admits a pointwise left Kan extension along `L`, then any left Kan extension of `F`
along `L` is a pointwise left Kan extension.  -/
CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                [L.HasPointwiseLeftKanExtension F] →
                  (F' : CategoryTheory.Functor D H) →
                    (α : F ⟶ L.comp F') →
                      [F'.IsLeftKanExtension α] →
                        (CategoryTheory.Functor.LeftExtension.mk F' α).IsPointwiseLeftKanExtension
-- Mathlib.LinearAlgebra.TensorProduct.Pi
TensorProduct.piScalarRight_apply : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] (ι : Type u_4)
  [inst_7 : Fintype ι] [inst_8 : DecidableEq ι] (x : TensorProduct R N (ι → R)),
  (TensorProduct.piScalarRight R S N ι) x = (TensorProduct.piScalarRightHom R S N ι) x
-- Mathlib.Data.Nat.Bitwise
Nat.bit_mod_two_eq_zero_iff : ∀ (a : Bool) (x : ℕ), Nat.bit a x % 2 = 0 ↔ (!a) = true
-- Mathlib.Analysis.Calculus.Deriv.Add
derivWithin_const_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (c : F),
  derivWithin (fun y => c - f y) s x = -derivWithin f s x
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Reorder a sum.

The difference with `Finset.sum_nbij'` is that the bijection is specified as a surjective injection,
rather than by an inverse function.

The difference with `Finset.sum_bij` is that the bijection is a non-dependent function, rather than
being allowed to use membership of the domain of the sum.  -/
Finset.sum_nbij : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (i : ι → κ),
  (∀ a ∈ s, i a ∈ t) → Set.InjOn i ↑s → Set.SurjOn i ↑s ↑t → (∀ a ∈ s, f a = g (i a)) → ∑ x ∈ s, f x = ∑ x ∈ t, g x
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.scott_eq_upper_of_completeLinearOrder : ∀ {α : Type u_1} [inst : CompleteLinearOrder α], Topology.scott α Set.univ = Topology.upper α
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Empty.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicOnNhd.harmonicContOnCl : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicOnNhd f (closure s) → InnerProductSpace.HarmonicContOnCl f s
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.lhs : Nat.Internal.Linear.PolyCnstr → Nat.Internal.Linear.Poly
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k},
  (Std.ExtDTreeMap.filterMap f t).getD k fallback = ((t.get? k).bind (f k)).getD fallback
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.killCompl_map : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  {f : σ → τ} (hf : Function.Injective f) (φ : R →+* S) (p : MvPolynomial τ R),
  (MvPolynomial.killCompl hf) ((MvPolynomial.map φ) p) = (MvPolynomial.map φ) ((MvPolynomial.killCompl hf) p)
-- Mathlib.Probability.Distributions.Gaussian.Fernique
/-- Characteristic function of a centered Gaussian measure.  -/
ProbabilityTheory.IsGaussian.charFunDual_eq_of_integral_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E],
  ∫ (x : E), id x ∂μ = 0 →
    ∀ (L : StrongDual ℝ E), MeasureTheory.charFunDual μ L = Complex.exp (-↑(ProbabilityTheory.variance (⇑L) μ) / 2)
-- Lean.Data.PPContext
Lean.PPContext.mk : Lean.Environment →
  Lean.MetavarContext → Lean.LocalContext → Lean.Options → Lean.Name → List Lean.OpenDecl → Lean.PPContext
-- Aesop.Builder.Basic
Aesop.RuleBuilderOptions.mk.inj : ∀ {immediatePremises? : Option (Array Lean.Name)} {indexingMode? : Option Aesop.IndexingMode}
  {casesPatterns? : Option (Array Aesop.CasesPattern)} {pattern? : Option Lean.Term}
  {transparency? indexTransparency? : Option Lean.Meta.TransparencyMode}
  {immediatePremises?_1 : Option (Array Lean.Name)} {indexingMode?_1 : Option Aesop.IndexingMode}
  {casesPatterns?_1 : Option (Array Aesop.CasesPattern)} {pattern?_1 : Option Lean.Term}
  {transparency?_1 indexTransparency?_1 : Option Lean.Meta.TransparencyMode},
  { immediatePremises? := immediatePremises?, indexingMode? := indexingMode?, casesPatterns? := casesPatterns?,
        pattern? := pattern?, transparency? := transparency?, indexTransparency? := indexTransparency? } =
      { immediatePremises? := immediatePremises?_1, indexingMode? := indexingMode?_1,
        casesPatterns? := casesPatterns?_1, pattern? := pattern?_1, transparency? := transparency?_1,
        indexTransparency? := indexTransparency?_1 } →
    immediatePremises? = immediatePremises?_1 ∧
      indexingMode? = indexingMode?_1 ∧
        casesPatterns? = casesPatterns?_1 ∧
          pattern? = pattern?_1 ∧ transparency? = transparency?_1 ∧ indexTransparency? = indexTransparency?_1
-- Mathlib.RingTheory.PicardGroup
instSmallUnitsSkeletonSemimoduleCat : ∀ (R : Type u) [inst : CommSemiring R], Small.{u, u + 1} (CategoryTheory.Skeleton (SemimoduleCat R))ˣ
-- Lean.Data.KVMap
Lean.DataValue.beqExp : Lean.DataValue → Lean.DataValue → Bool
-- Init.Data.List.Range
List.tail_zipIdx : ∀ {α : Type u_1} {l : List α} {i : ℕ}, (l.zipIdx i).tail = l.tail.zipIdx (i + 1)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_base_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  {s : CategoryTheory.Limits.WidePullbackCone f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (b : W ⟶ X)
  (a : (i : ι) → W ⟶ Y i) (w : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a i) (f i) = b) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullbackCone.IsLimit.lift hs b a w)
      (CategoryTheory.CategoryStruct.comp s.base h) =
    CategoryTheory.CategoryStruct.comp b h
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Ico_eq_Iio_self_iff : ∀ {ι : Sort u} {α : Type v} [inst : LinearOrder α] {f : ι → α} {a : α},
  ⋃ i, Set.Ico (f i) a = Set.Iio a ↔ ∀ x < a, ∃ i, f i ≤ x
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- The mapping between the vectors of the bases.  -/
Module.Basis.SmithNormalForm.f : {R : Type u_2} →
  [inst : CommRing R] →
    {M : Type u_3} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {N : Submodule R M} → {ι : Type u_4} → {n : ℕ} → Module.Basis.SmithNormalForm N ι n → Fin n ↪ ι
-- Mathlib.CategoryTheory.Limits.Indization.Category
/-- The inclusion of `C` into `Ind C` induced by the Yoneda embedding.  -/
CategoryTheory.Ind.yoneda : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (CategoryTheory.Ind C)
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.ofHom.eq_1 : ∀ {X Y : Type u} [inst : AddGroup X] [inst_1 : AddGroup Y] (f : X →+ Y),
  AddGrpCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f
-- Mathlib.Topology.UniformSpace.Basic
uniformity_prod_eq_prod : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β],
  uniformity (α × β) = Filter.map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (uniformity α ×ˢ uniformity β)
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_zero : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω), P⁻[0 | mΩ] = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.whisker_pt : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f)
  (g : K ≃ J), (c.whisker g).pt = c.pt
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
/-- If `C` is a Grothendieck abelian category, `X : C`, if `F : J ⥤ MonoOver X` is a
functor from a `κ`-filtered category `J` with `κ` a regular cardinal such
that `HasCardinalLT (Subobject X) κ`, and if the colimit of `F` (computed in `C`)
maps epimorphically onto `X`, then there exists `j : J` such that `(F.obj j).obj.hom`
is an isomorphism.  -/
CategoryTheory.IsGrothendieckAbelian.exists_isIso_of_functor_from_monoOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w} [inst_3 : CategoryTheory.SmallCategory J]
  (F : CategoryTheory.Functor J (CategoryTheory.MonoOver X)) {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ],
  HasCardinalLT (CategoryTheory.Subobject X) κ →
    ∀
      (c :
        CategoryTheory.Limits.Cocone (F.comp ((CategoryTheory.MonoOver.forget X).comp (CategoryTheory.Over.forget X))))
      (hc : CategoryTheory.Limits.IsColimit c) (f : c.pt ⟶ X),
      (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) f = (F.obj j).obj.hom) →
        CategoryTheory.Epi f → ∃ j, CategoryTheory.IsIso (F.obj j).obj.hom
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_eq_getElem! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {a : α} {h : a ∈ t}, t[a] = t[a]!
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.basicOpen_one : ∀ {R : Type u} [inst : CommSemiring R], PrimeSpectrum.basicOpen 1 = ⊤
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_nsmul_coe_div_two : ∀ (θ : ℝ), 2 • ↑(θ / 2) = ↑θ
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.affine_isReduced_iff : ∀ (R : CommRingCat), AlgebraicGeometry.IsReduced (AlgebraicGeometry.Spec R) ↔ IsReduced ↑R
-- Lean.Server.Completion.CompletionCollectors
Lean.Server.Completion.dotCompletion : Lean.Lsp.DocumentUri →
  Lean.Lsp.Position →
    ℕ → Lean.Elab.ContextInfo → Lean.Elab.TermInfo → Lean.Server.CancellableM (Array Lean.Lsp.ResolvableCompletionItem)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- An algebra morphism with an underlying epimorphism hom in `C` is an algebra epimorphism.  -/
CategoryTheory.Endofunctor.Coalgebra.epi_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {X Y : CategoryTheory.Endofunctor.Coalgebra F} (f : X ⟶ Y) [h : CategoryTheory.Epi f.f], CategoryTheory.Epi f
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.rightUnitorNatIso_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategory.rightUnitorNatIso C).inv.app X =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α},
  t.WF → (Std.DTreeMap.Raw.filterMap f t).contains k = Option.any (fun x => (f k x).isSome) (t.get? k)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.congr_fun : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {f g : A₁ ≃ₐ[R] A₂}, f = g → ∀ (x : A₁), f x = g x
-- Mathlib.CategoryTheory.Shift.Basic
/-- the composition of shift functors identifies to the shift by the sum  -/
CategoryTheory.ShiftMkCore.add : {C : Type u} →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] →
        (self : CategoryTheory.ShiftMkCore C A) → (n m : A) → self.F (n + m) ≅ (self.F n).comp (self.F m)
-- Mathlib.Algebra.Order.UpperLower
lowerClosure_one : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α], lowerClosure 1 = 1
-- Mathlib.Algebra.Ring.CharZero
units_ne_neg_self : ∀ {R : Type u_2} [inst : Ring R] [CharZero R] (u : Rˣ), u ≠ -u
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- `M →ₛₗ[σ] N` is the type of `σ`-semilinear maps from `M` to `N`.  -/
«term_→ₛₗ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Closure
interior_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, interior s ⊆ s
-- Mathlib.Condensed.Discrete.LocallyConstant
CondensedSet.LocallyConstant.instFaithfulFunctor : CondensedSet.LocallyConstant.functor.Faithful
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_comp_le_tsum_of_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Injective f → ∀ (g : β → ENNReal), ∑' (x : α), g (f x) ≤ ∑' (y : β), g y
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.addX_neg : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R},
  W'.Equation P → W'.addX P (W'.neg P) = W'.dblZ P ^ 2
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_sSup_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U : Set (Submodule 𝕜 E)} {V : Submodule 𝕜 E}, sSup U ⟂ V ↔ ∀ Uᵢ ∈ U, Uᵢ ⟂ V
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_mul_unit_right_right : ∀ {R : Type u_1} [inst : CommSemiring R] {x : R}, IsUnit x → ∀ (y z : R), IsCoprime y (z * x) ↔ IsCoprime y z
-- Init.Data.Vector.Lemmas
Vector.foldr_hom : ∀ {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} {n : ℕ} (f : β₁ → β₂) {g₁ : α → β₁ → β₁} {g₂ : α → β₂ → β₂}
  {xs : Vector α n} {init : β₁},
  (∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)) → Vector.foldr g₂ (f init) xs = f (Vector.foldr g₁ init xs)
-- Mathlib.Analysis.Convex.Function
/-- A strictly convex function on an open segment is strictly upper-bounded by the max of its
endpoints.  -/
StrictConvexOn.lt_on_open_segment' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  StrictConvexOn 𝕜 s f →
    ∀ {x y : E}, x ∈ s → y ∈ s → x ≠ y → ∀ {a b : 𝕜}, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < max (f x) (f y)
-- Batteries.Tactic.PrintDependents
Batteries.Tactic.CollectDependents.State.mk : Bool → Lean.NameMap Bool → Batteries.Tactic.CollectDependents.State
-- Mathlib.CategoryTheory.Monoidal.Braided.Transport
/-- This is a def because once we have that both `(e' e).inverse` and `(e' e).functor` are
braided, this causes a diamond.
 -/
CategoryTheory.Monoidal.transportedFunctorCompInverseBraided : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (e : C ≌ D) →
          [inst_2 : CategoryTheory.MonoidalCategory C] →
            [inst_3 : CategoryTheory.BraidedCategory C] →
              ((CategoryTheory.Monoidal.equivalenceTransported e).functor.comp
                  (CategoryTheory.Monoidal.equivalenceTransported e).inverse).Braided
-- Batteries.Tactic.Trans
Batteries.Tactic.TransRelation.app.injEq : ∀ (rel rel_1 : Lean.Expr),
  (Batteries.Tactic.TransRelation.app rel = Batteries.Tactic.TransRelation.app rel_1) = (rel = rel_1)
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- The product of a finite family of charted spaces is naturally a charted space, with the
canonical construction of the atlas of finite product maps.  -/
piChartedSpace : {ι : Type u_5} →
  [Finite ι] →
    (H : ι → Type u_6) →
      [inst : (i : ι) → TopologicalSpace (H i)] →
        (M : ι → Type u_7) →
          [inst_1 : (i : ι) → TopologicalSpace (M i)] →
            [(i : ι) → ChartedSpace (H i) (M i)] → ChartedSpace (ModelPi H) ((i : ι) → M i)
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instOneOfNatIntOfHasDetPlusMinusOneFinNatReal : {Γ : Subgroup (GL (Fin 2) ℝ)} → [Γ.HasDetPlusMinusOne] → One (SlashInvariantForm Γ 0)