mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Ring.Basic
/-- An injective non-unital ring homomorphism from a `Ring` to a `NormedRing` induces a
`NormedRing` structure on the domain.

See note [reducible non-instances]  -/
NormedRing.induced : {F : Type u_5} →
  (R : Type u_6) →
    (S : Type u_7) →
      [inst : FunLike F R S] →
        [inst_1 : Ring R] →
          [inst_2 : NormedRing S] → [NonUnitalRingHomClass F R S] → (f : F) → Function.Injective ⇑f → NormedRing R
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft.eq_1 : ∀ (x n : ℕ), (Int.ofNat n).shiftLeft x = Int.ofNat (n <<< x)
-- Std.Time.Format.Modifier
/-- Parses a single format `Modifier` from the input string.  -/
Std.Time.parseModifier : Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_isoPushout_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inl f g))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q hP.isoPushout.inv) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inl
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- Given two monomorphisms `S` and `T` over `X` and `Y` and two morphisms `f` and `f'` between them
forming the following pullback square:

```
(T : C) -f'-> (S : C)
   |             |
T.arrow       S.arrow
   |             |
   v             v
   Y -----f----> X
```

we get an isomorphism between `T` and the pullback of `S` along `f` through the `pullback` functor.
 -/
CategoryTheory.MonoOver.pullbackObjIsoOfIsPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {X Y : C} →
        (f : Y ⟶ X) →
          (S : CategoryTheory.MonoOver X) →
            (T : CategoryTheory.MonoOver Y) →
              (f' : T.obj.left ⟶ S.obj.left) →
                CategoryTheory.IsPullback f' T.arrow S.arrow f → ((CategoryTheory.MonoOver.pullback f).obj S ≅ T)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
sup_sq_eq_mul_mul_mabs_div : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a b : α), (a ⊔ b) ^ 2 = a * b * |b / a|ₘ
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.le_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {k fallback : α}, (cmp k (t.minD fallback)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Data.Set.Image
Set.image_eta : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} (f : α → β), f '' s = (fun x => f x) '' s
-- Mathlib.Data.Finset.Sum
Finset.disjoint_map_inl_map_inr : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β),
  Disjoint (Finset.map Function.Embedding.inl s) (Finset.map Function.Embedding.inr t)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.liftWith_refl : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPred} (f : ({β : Type u} → m β → m β) → m α),
  ⦃ Std.Internal.Do.wp (f fun {β} x => x) post epost ⦄ liftWith f ⦃ post; epost ⦄
-- Init.Data.Order.Lemmas
Std.instIdempotentOpMinOfMinEqOr : ∀ {α : Type u} [inst : Min α] [Std.MinEqOr α], Std.IdempotentOp min
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.isoMk_inv : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} (f : F X ≅ F Y),
  (CategoryTheory.InducedCategory.isoMk f).inv = CategoryTheory.InducedCategory.homMk f.inv
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedExSum : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} → Inhabited ((e : Q(«$α»)) × Mathlib.Tactic.Ring.Common.ExSum bt sα e)
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.coe_finite_iff : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} {pt : DiscreteTiling.PlacedTile ps}, (↑pt).Finite ↔ (↑(↑ps pt.index)).Finite
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
/-- If `x` and `y` are two points in a finite-dimensional space over `ℝ`, then `Euclidean.dist x y`
is the distance between these points in the metric defined by some inner product space structure on
`E`.  -/
Euclidean.dist : {E : Type u_1} →
  [inst : AddCommGroup E] →
    [inst_1 : TopologicalSpace E] →
      [IsTopologicalAddGroup E] →
        [T2Space E] → [inst_4 : Module ℝ E] → [ContinuousSMul ℝ E] → [FiniteDimensional ℝ E] → E → E → ℝ
-- Init.Notation
/-- `a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`. -/
«term_⁻¹» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- Eta-expanded form of `differentiableAt_id` -/
differentiableAt_fun_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E}, DifferentiableAt 𝕜 (fun x => x) x
-- Mathlib.Analysis.Calculus.Deriv.Comp
deriv_comp_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {y : 𝕜'},
  DifferentiableAt 𝕜' h₂ y → DifferentiableAt 𝕜 h x → h x = y → deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x
-- Mathlib.CategoryTheory.Core
CategoryTheory.Iso.core_inv_app_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : CategoryTheory.Core C),
  (α.core.inv.app X).iso.hom = α.inv.app X.of
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.run : Lean.MVarId → Lean.Elab.Tactic.TacticM Unit → Lean.Elab.TermElabM (List Lean.MVarId)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_alter_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option (β k) → Option (β k)}, m.WF → (m.alter k f).get? k = f (m.get? k)
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.brecOn.go : {motive_1 : Lean.Widget.MsgEmbed → Sort u} →
  {motive_2 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed → Sort u} →
    {motive_3 :
        Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
            (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) →
          Sort u} →
      {motive_4 : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u} →
        {motive_5 : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u} →
          (t : Lean.Widget.MsgEmbed) →
            ((t : Lean.Widget.MsgEmbed) → t.below → motive_1 t) →
              ((t : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Lean.Widget.MsgEmbed.below_1 t → motive_2 t) →
                ((t :
                      Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
                        (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)) →
                    Lean.Widget.MsgEmbed.below_2 t → motive_3 t) →
                  ((t : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) →
                      Lean.Widget.MsgEmbed.below_3 t → motive_4 t) →
                    ((t : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) →
                        Lean.Widget.MsgEmbed.below_4 t → motive_5 t) →
                      motive_1 t ×' t.below
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.mapAddHom_mapAddHom : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Add α] [inst_1 : Add β] [inst_2 : Add γ] (f : α →ₙ+ β) (g : β →ₙ+ γ)
  (x : WithZero α), (WithZero.mapAddHom g) ((WithZero.mapAddHom f) x) = (WithZero.mapAddHom (g.comp f)) x
-- Mathlib.Data.Finset.Density
Finset.card_mul_dens : ∀ {α : Type u_2} [inst : Fintype α] (s : Finset α), ↑(Fintype.card α) * s.dens = ↑s.card
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.instPreservesColimitWalkingSpanSpanAppMapFunctorCurriedTensorHomLeftObjOfWhiskerRightWhiskerLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X₁ X₂ : CategoryTheory.Arrow C) {F : CategoryTheory.Functor C C}
  [CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      F],
  CategoryTheory.Limits.PreservesColimit
    (CategoryTheory.Limits.span (((CategoryTheory.MonoidalCategory.curriedTensor C).map X₁.hom).app X₂.left)
      (((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁.left).map X₂.hom))
    F
-- Init.Data.UInt.Lemmas
UInt32.lt_of_lt_of_le : ∀ {a b c : UInt32}, a < b → b ≤ c → a < c
-- Init.Data.Int.Cooper
Int.Cooper.resolve_left'.congr_simp : ∀ (a a_1 : ℤ) (e_a : a = a_1) (c c_1 : ℤ),
  c = c_1 →
    ∀ (d d_1 : ℤ),
      d = d_1 →
        ∀ (p p_1 : ℤ) (e_p : p = p_1) (x x_1 : ℤ) (e_x : x = x_1) (h₁ : p ≤ a * x),
          Int.Cooper.resolve_left' a c d p x h₁ = Int.Cooper.resolve_left' a_1 c_1 d_1 p_1 x_1 ⋯
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Tower law: if `A` is a `K`-module and `K` is an extension of `F` then
$\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

This is a simpler version of `lift_rank_mul_lift_rank` with `K` and `A` in the same universe.  -/
rank_mul_rank : ∀ (F : Type u) (K : Type v) [inst : Semiring F] [inst_1 : Semiring K] [inst_2 : Module F K] [StrongRankCondition F]
  [StrongRankCondition K] [Module.Free F K] (A : Type v) [inst_6 : AddCommMonoid A] [inst_7 : Module K A]
  [inst_8 : Module F A] [IsScalarTower F K A] [Module.Free K A], Module.rank F K * Module.rank K A = Module.rank F A
-- Mathlib.RingTheory.Etale.Weakly
Algebra.WeaklyEtale.flat_lmul' : ∀ (R : Type u_3) (S : Type u_4) {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  [self : Algebra.WeaklyEtale R S], (Algebra.TensorProduct.lmul' R).Flat
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_inv_app_hom_app_hom_apply_down : ∀ {C : Type u} [inst : CategoryTheory.Category.{max w v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : C) (X_1 : Cᵒᵖ) (x : Opposite.unop X_1 ⟶ X),
  ((CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaIsoYoneda.inv.app X).hom.app X_1)) x).down = x
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.Indep.isBase_of_cRank_le_of_finite : ∀ {α : Type u} {M : Matroid α} {I : Set α}, M.Indep I → M.cRank ≤ Cardinal.mk ↑I → I.Finite → M.IsBase I
-- Mathlib.Topology.Sion
/-- Under suitable inequalities, `setOfPred_sublevelLeft_subset` is closed  -/
_private.Mathlib.Topology.Sion.0.Sion.isClosed_setOfPred_sublevelLeft_subset : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β}
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E],
  X.Nonempty →
    IsCompact X →
      (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
        (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
          ∀ [inst_6 : TopologicalSpace F] [inst_7 : AddCommGroup F] [inst_8 : Module ℝ F],
            Convex ℝ Y →
              (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
                (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
                  ∀ (a : E) (b b' : β) (y y' : ↑Y),
                    (∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')) →
                      (∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b) →
                        b' < max (f a ↑y) (f a ↑y') →
                          b < b' → IsClosed (Sion.setOfPred_sublevelLeft_subset✝ X Y f b b' y y')
-- Init.Data.SInt.Lemmas
ISize.toBitVec_zero : ISize.toBitVec 0 = 0#System.Platform.numBits
-- Mathlib.RingTheory.KrullDimension.Regular
Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {M : Type u_2} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.Finite R M] {x : R},
  (∀ p ∈ (Module.annihilator R M).minimalPrimes, x ∉ p) →
    x ∈ (Module.annihilator R M).jacobson → Module.supportDim R (QuotSMulTop x M) + 1 = Module.supportDim R M
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLT?.go.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option α) (a : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getKeyLT?.go k best a =
    match a with
    | Std.DTreeMap.Internal.Impl.leaf => best
    | Std.DTreeMap.Internal.Impl.inner size ky v l r =>
      match compare k ky with
      | Ordering.gt => Std.DTreeMap.Internal.Impl.getKeyLT?.go k (some ky) r
      | x => Std.DTreeMap.Internal.Impl.getKeyLT?.go k best l
-- Mathlib.RingTheory.Finiteness.Basic
_private.Mathlib.RingTheory.Finiteness.Basic.0.instModuleFiniteAux : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedRing R], Module.Finite { c // 0 ≤ c } R
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instSurjectiveDescI₀SchemeF : ∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X),
  AlgebraicGeometry.Surjective (CategoryTheory.Limits.Sigma.desc fun i => 𝒰.f i)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.one : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop} (j : J),
  CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_lt_pow_iff_norm_le_pow_sub_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℤ), ‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)
-- Mathlib.Data.Fin.Tuple.Basic
/-- For `m : Fin n`, if `m` satisfies `p`, then `Fin.find p h ≤ m`.  -/
Fin.find_le_of_pos : ∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] (h : ∃ k, p k) {j : Fin n}, p j → Fin.find p h ≤ j
-- Mathlib.Algebra.Ring.Defs
/-- An element of a ring multiplied by the additive inverse of one is the element's additive
inverse.  -/
mul_neg_one : ∀ {α : Type u} [inst : MulOneClass α] [inst_1 : HasDistribNeg α] (a : α), a * -1 = -a
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
/-- The t-structure induced on the full subcategory of `t`-bounded objects.  -/
CategoryTheory.Triangulated.TStructure.onBounded : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                [CategoryTheory.IsTriangulated C] → CategoryTheory.Triangulated.TStructure t.bounded.FullSubcategory
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instT3Space : ∀ (E : Type u_5) (F : Type u_6) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F], T3Space (SchwartzMap E F)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.any_eq_true_iff_exists_mem_getKey_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulHashable α]
  [EquivBEq α] {p : α → β → Bool},
  m.WF → (m.any p = true ↔ ∃ a, ∃ (h : a ∈ m), p (m.getKey a h) (Std.DHashMap.Raw.Const.get m a h) = true)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_intCast : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (z : ℤ), (↑z).imK = 0
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.toOplax_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.StrongTrans F G) (a : B), η.toOplax.app a = η.app a
-- Mathlib.Order.Sublattice
Sublattice.map_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (L M : Sublattice α) (f : LatticeHom α β),
  Function.Injective ⇑f → Sublattice.map f (L ⊓ M) = Sublattice.map f L ⊓ Sublattice.map f M
-- Mathlib.FieldTheory.Separable
Polynomial.separable_one : ∀ {R : Type u} [inst : CommSemiring R], Polynomial.Separable 1
-- Lean.PrettyPrinter.Delaborator.FieldNotation
/-- Returns the field name of the projection if `e` is an application that is a projection to a parent structure.
If `explicit` is `true`, then requires that the structure have no parameters.
 -/
Lean.PrettyPrinter.Delaborator.parentProj? : Bool → Lean.Expr → Lean.MetaM (Option Lean.Name)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceE_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceE._auto_3),
  (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₃ =
    ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₃) ⊞ (X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f₁))
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.isOpen_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set Y},
  IsOpen (⇑h ⁻¹' s) ↔ IsOpen s
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Coreflective.comparison_full : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {R : CategoryTheory.Functor D C} [R.Full] {L : CategoryTheory.Functor C D} (adj : R ⊣ L),
  (CategoryTheory.Comonad.comparison adj).Full
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.IsLocalSourceTargetProperty.congr : ∀ {H : Type u_6} {G : Type u_8} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace G] {M : Type u_10}
  {N : Type u_12} [inst_2 : TopologicalSpace M] [inst_3 : TopologicalSpace N]
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop},
  Manifold.IsLocalSourceTargetProperty P →
    ∀ {f g : M → N} {φ : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G},
      Set.EqOn f g φ.source → P f φ ψ → P g φ ψ
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.collectGuards : Lean.Meta.Grind.EMatchTheorem → Lean.Expr → Array Lean.Expr → Lean.Meta.Grind.GoalM (List Lean.Meta.Grind.TheoremGuard)
-- Lean.DocString.Types
Lean.Doc.Part.brecOn_1.go : {i : Type u} →
  {b : Type v} →
    {p : Type w} →
      {motive_1 : Lean.Doc.Part i b p → Sort u_1} →
        {motive_2 : Array (Lean.Doc.Part i b p) → Sort u_1} →
          {motive_3 : List (Lean.Doc.Part i b p) → Sort u_1} →
            (t : Array (Lean.Doc.Part i b p)) →
              ((t : Lean.Doc.Part i b p) → t.below → motive_1 t) →
                ((t : Array (Lean.Doc.Part i b p)) → Lean.Doc.Part.below_1 t → motive_2 t) →
                  ((t : List (Lean.Doc.Part i b p)) → Lean.Doc.Part.below_2 t → motive_3 t) →
                    motive_2 t ×' Lean.Doc.Part.below_1 t
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedMVarErrorInfo.default : Lean.Elab.Term.MVarErrorInfo
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_nat_mod : ∀ (s : Multiset ℕ) (n : ℕ), s.prod % n = (Multiset.map (fun x => x % n) s).prod % n
-- Init.Meta.Defs
/-- Expand `interpStr` into a term of type `type` (which supports ` ++ `),
calling `ofInterpFn` on terms within `{}`,
and `ofLitFn` on the literals between the interpolations.  -/
Lean.TSyntax.expandInterpolatedStr : Lean.TSyntax Lean.interpolatedStrKind →
  Lean.Term → (ofInterpFn : Lean.Term) → optParam Lean.Term ofInterpFn → Lean.MacroM Lean.Term
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.inclusion_injective : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A}
  (h : S ≤ T), Function.Injective ⇑(Subalgebra.inclusion h)
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- If `G` is an additive group with measurable addition, then addition of `g : G`
on the left is a measurable automorphism of `G`.  -/
MeasurableEquiv.addLeft : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : MeasurableSpace G] → [MeasurableAdd G] → G → G ≃ᵐ G
-- Mathlib.FieldTheory.Relrank
Subfield.lift_relrank_comap_comap_eq_lift_relrank_of_surjective : ∀ {E : Type v} [inst : Field E] {L : Type w} [inst_1 : Field L] (A B : Subfield E) (f : L →+* E),
  Function.Surjective ⇑f →
    Cardinal.lift.{v, w} ((Subfield.comap f A).relrank (Subfield.comap f B)) = Cardinal.lift.{w, v} (A.relrank B)
-- Mathlib.Data.Finsupp.Multiset
Multiset.toFinsupp_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (a : α), (Multiset.toFinsupp s) a = Multiset.count a s
-- Init.SimpLemmas
Lean.arrow_congr_left : ∀ {p₁ p₂ : Sort u} {q : Sort v}, p₁ = p₂ → Lean.Arrow p₁ q = Lean.Arrow p₂ q
-- Mathlib.Analysis.Normed.Group.Defs
/-- An e-seminormed monoid is a monoid endowed with a continuous enorm.
Note that we only ask for the enorm to be a semi-norm: non-trivial elements may have enorm zero.  -/
ESeminormedMonoid : (E : Type u_8) → [TopologicalSpace E] → Type u_8
-- Mathlib.Analysis.Convex.Function
/-- **Alias** of the reverse direction of `neg_convexOn_iff`.

---

A function `-f` is convex iff `f` is concave.  -/
ConcaveOn.neg : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f : E → β}, ConcaveOn 𝕜 s f → ConvexOn 𝕜 s (-f)
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D), (J.sheafificationWhiskerRightIso F).inv.app P = (J.sheafifyCompIso F P).inv
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.iSup_adj : ∀ {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {a b : V} {f : ι → G.Subgraph},
  (⨆ i, f i).Adj a b ↔ ∃ i, (f i).Adj a b