mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instIsOrderedMonoidValueGroupWithZero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R], IsOrderedMonoid (ValuativeRel.ValueGroupWithZero R)
-- Mathlib.RingTheory.Algebraic.MvPolynomial
MvPolynomial.transcendental_supported_polynomial_aeval_X_iff : ∀ {σ : Type u_1} (R : Type u_2) [inst : CommRing R] [Nontrivial R] {i : σ} {s : Set σ} {f : Polynomial R},
  Transcendental (↥(MvPolynomial.supported R s)) ((Polynomial.aeval (MvPolynomial.X i)) f) ↔ i ∉ s ∧ Transcendental R f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k : α} {v : β}, (t.insert k v)[k] = v
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (μ : MeasureTheory.Measure α),
  μ.prod 0 = 0
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousOn_biInf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {ι : Sort u_4} {δ : Type u_5} [inst_1 : CompleteLinearOrder δ]
  {p : ι → Prop} {f : (i : ι) → p i → α → δ},
  (∀ (i : ι) (hi : p i), UpperSemicontinuousOn (f i hi) s) →
    UpperSemicontinuousOn (fun x' => ⨅ i, ⨅ (hi : p i), f i hi x') s
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.addZeroClass : {α : Type u} → [MulOneClass α] → AddZeroClass (Additive α)
-- Std.Data.HashSet.Raw
/-- Carries out a monadic action on each element in the hash set in some order.  -/
Std.HashSet.Raw.forM : {α : Type u} → {m : Type v → Type w} → [Monad m] → (α → m PUnit.{v + 1}) → Std.HashSet.Raw α → m PUnit.{v + 1}
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.equal.injEq : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (t₁ t₂ t₁_1 t₂_1 : L.Term (α ⊕ Fin n)),
  (FirstOrder.Language.BoundedFormula.equal t₁ t₂ = FirstOrder.Language.BoundedFormula.equal t₁_1 t₂_1) =
    (t₁ = t₁_1 ∧ t₂ = t₂_1)
-- Mathlib.Order.Concept
Concept.intent_ofAttributes_of_isIntent : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β},
  Order.IsIntent r t → (Concept.ofAttributes r t).intent = t
-- Init.Data.Option.Lemmas
Option.elim_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} {f : α → β} {g' : γ} {g : β → γ} (o : Option α),
  (Option.map f o).elim g' g = o.elim g' (g ∘ f)
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_unique : ∀ {α : Type u_1} [Nonempty α] [Subsingleton α], Nat.card α = 1
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.toSkeletonFunctor_map_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.toSkeletonFunctor C).map f).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.fromSkeletonToSkeletonIso X).hom
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.fromSkeletonToSkeletonIso Y).inv)
-- Mathlib.Data.Sym.Sym2
Sym2.mem_and_mem_iff : ∀ {α : Type u_1} {x y : α} {z : Sym2 α}, x ≠ y → (x ∈ z ∧ y ∈ z ↔ z = s(x, y))
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
/-- Auxiliary definition for `sqFunctor`.  -/
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {F : CategoryTheory.Functor J C} →
            {c : CategoryTheory.Limits.Cocone F} →
              {X Y : C} →
                {p : X ⟶ Y} →
                  {f : F.obj ⊥ ⟶ X} →
                    {g : c.pt ⟶ Y} →
                      {j : J} →
                        CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j →
                          {j' : J} →
                            (j' ⟶ j) → CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j'
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) {n : ℕ} (x : ↑(F.H' n S.X₂ ⊞ F.H' n S.X₃)),
  (CategoryTheory.Abelian.Ext.mk₀ S.shortComplex.f).comp
      (CategoryTheory.Abelian.Ext.biprodAddEquiv.symm
        ((CategoryTheory.ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom) x))
      ⋯ =
    (CategoryTheory.ConcreteCategory.hom (S.fromBiprod F n)) x
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.Faithful.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} [F.Faithful] (α : F ≅ F'), F'.Faithful
-- Mathlib.SetTheory.ZFC.Class
Class.instIsWellFoundedMem : IsWellFounded Class.{u_1} fun x1 x2 => x1 ∈ x2
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.closedBall_one_div : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → Metric.closedBall 1 δ / s = Metric.cthickening δ s⁻¹
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.Functor.FullyFaithful.mulEquivEnd_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (f_1 : f.obj X ⟶ f.obj X),
  (hf.mulEquivEnd X).symm f_1 = hf.preimage f_1
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Monomial degree of powers  -/
MonomialOrder.degree_pow_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R} (n : ℕ),
  m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)
-- Lean.Elab.Do.Basic
/-- Return true if we should generate an error message when lifting a nested action over this kind of syntax.  -/
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.nestedActionForbiddenBinder : Lean.Syntax → Bool
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.measure_sdiff`. -/
MeasureTheory.measure_diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  s₂ ⊆ s₁ → MeasureTheory.NullMeasurableSet s₂ μ → μ s₂ ≠ ⊤ → μ (s₁ \ s₂) = μ s₁ - μ s₂
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.le : ∀ (p q r : ENNReal) [p.HolderTriple q r], r ≤ p
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars_hom_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {X : ModuleCat R}
  {Y : ModuleCat S} (g : (ModuleCat.extendScalars f).obj X ⟶ Y) (x : ↑X),
  (ModuleCat.Hom.hom (ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) (1 ⊗ₜ[R] x)
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.range_projectionOntoL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q), (↑(p.projectionOntoL q h)).range = ⊤
-- Mathlib.Data.Num.ZNum
ZNum.div_zero : ∀ (n : ZNum), n / 0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.im_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasImages C]
  [inst_2 : CategoryTheory.Limits.HasImageMaps C] (f : CategoryTheory.Arrow C),
  CategoryTheory.Limits.im.obj f = CategoryTheory.Limits.image f.hom
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_top : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s : Finset β), (s.inf fun x => ⊤) = ⊤
-- Lean.DocString.Markdown
/-- A small, fixed heartbeat budget applied afresh to each custom element renderer.

Docstrings are rendered constantly (e.g. on every hover), and renderers may run arbitrary `MetaM`,
so this bounds the work any single element can impose.
 -/
Lean.Doc.mdRendererHeartbeats : ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideEqualizer.hom_ext_iff : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  [inst_1 : CategoryTheory.Limits.HasWideEqualizer f] [Nonempty J] {W : C}
  {k l : W ⟶ CategoryTheory.Limits.wideEqualizer f},
  k = l ↔
    CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.wideEqualizer.ι f) =
      CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.wideEqualizer.ι f)
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.instMonadAttachExceptTOfMonad.match_1.eq_1 : ∀ {m : Type (max u_1 u_2) → Type u_3} {ε : Type (max u_1 u_2)} [inst : MonadAttach m] {α : Type (max u_1 u_2)}
  (x : ExceptT ε m α) (motive : (a : Except ε α) → MonadAttach.CanReturn x a → Sort u_4) (a : α)
  (h : MonadAttach.CanReturn x (Except.ok a))
  (h_1 : (a : α) → (h : MonadAttach.CanReturn x (Except.ok a)) → motive (Except.ok a) h)
  (h_2 : (e : ε) → (h : MonadAttach.CanReturn x (Except.error e)) → motive (Except.error e) h),
  (match Except.ok a, h with
    | Except.ok a, h => h_1 a h
    | Except.error e, h => h_2 e h) =
    h_1 a h
-- Mathlib.MeasureTheory.Measure.NullMeasurable
Finset.nullMeasurableSet : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)] (s : Finset α),
  MeasureTheory.NullMeasurableSet (↑s) μ
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedSimprocs : Inhabited Lean.Meta.Simprocs
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.disjointSum_ground_eq : ∀ {α : Type u_1} {M N : Matroid α} {h : Disjoint M.E N.E}, (M.disjointSum N h).E = M.E ∪ N.E
-- Mathlib.Topology.NatEmbedding
/-- If `X` is an infinite Hausdorff topological space, then there exists a topological embedding
`f : ℕ → X`.

Note: this theorem is true for an infinite KC-space but the proof in that case is different.  -/
exists_topology_isEmbedding_nat : ∀ (X : Type u_1) [inst : TopologicalSpace X] [T2Space X] [Infinite X], ∃ f, Topology.IsEmbedding f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_app_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {X : Type u₇} {Y : Type u₈} [inst_6 : CategoryTheory.Category.{v₇, u₇} X]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} Y] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (U : CategoryTheory.Functor X Y) (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x : X),
  ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).hom.app
            X_1).snd.app
      x =
    CategoryTheory.CategoryStruct.id (ψ.right.obj (X_1.snd.obj (U.obj x)))
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.mk.injEq : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (baseSet : ι → Set B)
  (isOpen_baseSet : ∀ (i : ι), IsOpen (baseSet i)) (indexAt : B → ι)
  (mem_baseSet_at : ∀ (x : B), x ∈ baseSet (indexAt x)) (coordChange : ι → ι → B → F →L[R] F)
  (coordChange_self : ∀ (i : ι), ∀ x ∈ baseSet i, ∀ (v : F), (coordChange i i x) v = v)
  (continuousOn_coordChange : ∀ (i j : ι), ContinuousOn (coordChange i j) (baseSet i ∩ baseSet j))
  (coordChange_comp :
    ∀ (i j k : ι),
      ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k,
        ∀ (v : F), (coordChange j k x) ((coordChange i j x) v) = (coordChange i k x) v)
  (baseSet_1 : ι → Set B) (isOpen_baseSet_1 : ∀ (i : ι), IsOpen (baseSet_1 i)) (indexAt_1 : B → ι)
  (mem_baseSet_at_1 : ∀ (x : B), x ∈ baseSet_1 (indexAt_1 x)) (coordChange_1 : ι → ι → B → F →L[R] F)
  (coordChange_self_1 : ∀ (i : ι), ∀ x ∈ baseSet_1 i, ∀ (v : F), (coordChange_1 i i x) v = v)
  (continuousOn_coordChange_1 : ∀ (i j : ι), ContinuousOn (coordChange_1 i j) (baseSet_1 i ∩ baseSet_1 j))
  (coordChange_comp_1 :
    ∀ (i j k : ι),
      ∀ x ∈ baseSet_1 i ∩ baseSet_1 j ∩ baseSet_1 k,
        ∀ (v : F), (coordChange_1 j k x) ((coordChange_1 i j x) v) = (coordChange_1 i k x) v),
  ({ baseSet := baseSet, isOpen_baseSet := isOpen_baseSet, indexAt := indexAt, mem_baseSet_at := mem_baseSet_at,
        coordChange := coordChange, coordChange_self := coordChange_self,
        continuousOn_coordChange := continuousOn_coordChange, coordChange_comp := coordChange_comp } =
      { baseSet := baseSet_1, isOpen_baseSet := isOpen_baseSet_1, indexAt := indexAt_1,
        mem_baseSet_at := mem_baseSet_at_1, coordChange := coordChange_1, coordChange_self := coordChange_self_1,
        continuousOn_coordChange := continuousOn_coordChange_1, coordChange_comp := coordChange_comp_1 }) =
    (baseSet = baseSet_1 ∧ indexAt = indexAt_1 ∧ coordChange = coordChange_1)
-- Mathlib.GroupTheory.Congruence.Defs
Con.liftOnUnits.eq_1 : ∀ {M : Type u_1} {α : Type u_4} [inst : Monoid M] {c : Con M} (u : c.Quotientˣ)
  (f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α)
  (Hf :
    ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
      c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'),
  Con.liftOnUnits u f Hf = Con.hrecOn₂ (↑u) (↑u⁻¹) (fun x y hxy hyx => f x y ⋯ ⋯) ⋯ ⋯ ⋯
-- Mathlib.Algebra.MvPolynomial.Coeff
_private.Mathlib.Algebra.MvPolynomial.Coeff.0.MvPolynomial.coeff_linearCombination_X_pow_of_ne : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] {s : σ →₀ ℕ} (a : σ →₀ R) {n : ℕ},
  (s.sum fun x m => m) ≠ n → MvPolynomial.coeff s ((Finsupp.linearCombination R MvPolynomial.X) a ^ n) = 0
-- Mathlib.Analysis.Calculus.FDeriv.WithLp
hasFDerivWithinAt_piLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup H] [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedSpace 𝕜 H] [Finite ι] (p : ENNReal) [Fact (1 ≤ p)] {f : H → PiLp p E} {f' : H →L[𝕜] PiLp p E}
  {t : Set H} {y : H},
  HasFDerivWithinAt f f' t y ↔ ∀ (i : ι), HasFDerivWithinAt (fun x => (f x).ofLp i) (PiLp.proj p E i ∘SL f') t y
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then
`ω ↦ exp (t * |X| + v * X)` is integrable.  -/
ProbabilityTheory.integrable_exp_mul_abs_add : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v : ℝ},
  MeasureTheory.Integrable (fun ω => Real.exp ((v + t) * X ω)) μ →
    MeasureTheory.Integrable (fun ω => Real.exp ((v - t) * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp (t * |X ω| + v * X ω)) μ
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
NonUnitalStarSubsemiring.mk.sizeOf_spec : ∀ {R : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : Star R] [inst_2 : SizeOf R]
  (toNonUnitalSubsemiring : NonUnitalSubsemiring R)
  (star_mem' : ∀ {a : R}, a ∈ toNonUnitalSubsemiring.carrier → star a ∈ toNonUnitalSubsemiring.carrier),
  sizeOf { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := star_mem' } =
    1 + sizeOf toNonUnitalSubsemiring
-- Mathlib.Data.Multiset.Pi
/-- Given `δ : α → Sort*`, a multiset `m` and a term `a`, as well as a term `b : δ a` and a
function `f` such that `f a' : δ a'` for all `a'` in `m`, `Pi.cons m a b f` is a function `g` such
that `g a'' : δ a''` for all `a''` in `a ::ₘ m`.  -/
Multiset.Pi.cons : {α : Type u_1} →
  [DecidableEq α] →
    {δ : α → Sort u_2} → (m : Multiset α) → (a : α) → δ a → ((a : α) → a ∈ m → δ a) → (a' : α) → a' ∈ a ::ₘ m → δ a'
-- Std.Http.Protocol.H1.Parser
/-- Checks if a byte may appear unescaped inside a quoted-string value.

Allows `HTAB / SP / %x21 / %x23-5B / %x5D-7E` (strict ASCII-only; no obs-text).
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.isQdText : UInt8 → Bool
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
SimplyConnectedSpace.instSubsingletonQuotient : ∀ {X : Type u_3} [inst : TopologicalSpace X] [SimplyConnectedSpace X] (x y : X),
  Subsingleton (Path.Homotopic.Quotient x y)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.rightIso_hom : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ'),
  (CategoryTheory.Limits.CatCospanTransform.rightIso e).hom = e.hom.right
-- Lean.Elab.Term.TermElabM
/-- This type is an abbreviation for `Option Expr → TermElabM Expr`, but avoids a circular dependency
with `TermElabM`.

We store `FixedTermElabRef` in the `Context` of the `TermElabM` monad, inducing the circular
dependency. This mechanism allows us to register semantic term elaborators in
`el : Option Expr → TermElabM Expr` as scoped `s : Syntax`, such that `elabTerm s = el`.
 -/
Lean.Elab.Term.FixedTermElabRef : Type
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.lift_lsmul_comp_counit_comp_comul : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A],
  TensorProduct.lift (LinearMap.lsmul R A ∘ₗ CoalgebraStruct.counit) ∘ₗ CoalgebraStruct.comul = LinearMap.id
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type w) [inst_1 : CategoryTheory.Category.{w', w} J]
  [Small.{v, w} J] [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C],
  CategoryTheory.Limits.HasColimitsOfShape J (AlgebraicGeometry.SheafedSpace C)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.mkNatIso.congr_simp : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {J K : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)}
  (e₁ e₁_1 :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G))
  (e_e₁ : e₁ = e₁_1)
  (e₂ e₂_1 :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G))
  (e_e₂ : e₂ = e₂_1)
  (coh :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e₁.hom F)
        (CategoryTheory.CategoryStruct.comp (K.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
          (CategoryTheory.CategoryStruct.comp
            (K.whiskerLeft
              (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                  (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
            (K.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv)) =
      CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
        (CategoryTheory.CategoryStruct.comp
          (J.whiskerLeft
            (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
          (CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv
            (CategoryTheory.Functor.whiskerRight e₂.hom G)))),
  CategoryTheory.Limits.CategoricalPullback.mkNatIso e₁ e₂ coh =
    CategoryTheory.Limits.CategoricalPullback.mkNatIso e₁_1 e₂_1 ⋯
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.ExprWithAnchor.mk.sizeOf_spec : ∀ (e : Lean.Expr) (anchor : UInt64), sizeOf { e := e, anchor := anchor } = 1 + sizeOf e + sizeOf anchor
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.ciInf_eq_min'_image : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] (f : ι → α) {s : Finset ι},
  (∃ x ∈ s, f x ≤ sInf ∅) →
    ∀ (h' : autoParam (Finset.image f s).Nonempty Finset.ciInf_eq_min'_image._auto_1),
      ⨅ i ∈ s, f i = (Finset.image f s).min' h'
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.quotientPi_aux.right_inv : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] (p : (i : ι) → Submodule R (Ms i)) [inst_3 : Fintype ι] [inst_4 : DecidableEq ι],
  Function.RightInverse (Submodule.quotientPi_aux.invFun p) (Submodule.quotientPi_aux.toFun p)
-- Std.Data.TreeMap.Raw.Basic
/-- Checks whether a key is present in a map and inserts a value for the key if it was not found.
If the returned `Bool` is `true`, then the returned map is unaltered. If the `Bool` is `false`,
then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `contains` followed by `insertIfNew`.
 -/
Std.TreeMap.Raw.containsThenInsertIfNew : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → β → Bool × Std.TreeMap.Raw α β cmp
-- Mathlib.Order.Bounds.Basic
IsCofinalFor.nonempty : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, IsCofinalFor s t → s.Nonempty → t.Nonempty
-- Mathlib.Order.Grade
GradeOrder.wellFoundedLT : ∀ {α : Type u_3} [inst : Preorder α] (𝕆 : Type u_5) [inst_1 : Preorder 𝕆] [GradeOrder 𝕆 α] [WellFoundedLT 𝕆],
  WellFoundedLT α
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_union : ∀ {R : Type u} [inst : NonAssocSemiring R] (s t : Set R),
  Subsemiring.closure (s ∪ t) = Subsemiring.closure s ⊔ Subsemiring.closure t
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Poly.mulMon_denote.go : ∀ (ctx : Nat.Internal.Linear.Context) (k : ℕ) (m : Nat.Internal.SOM.Mon) (p acc : Nat.Internal.SOM.Poly),
  Nat.Internal.SOM.Poly.denote ctx (Nat.Internal.SOM.Poly.mulMon.go✝ k m p acc) =
    Nat.Internal.SOM.Poly.denote ctx acc + Nat.Internal.SOM.Poly.denote ctx p * k * Nat.Internal.SOM.Mon.denote ctx m
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isSome_getElem?_toList_rco_eq : ∀ {m n i : ℕ}, ((m...n).toList[i]?.isSome = true) = (i < n - m)
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.instInhabitedEntry.default : Lean.Meta.SimpAll.Entry
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.mono : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ ν₁ ν₂ : MeasureTheory.Measure α},
  μ₁.MutuallySingular ν₁ → μ₂ ≤ μ₁ → ν₂ ≤ ν₁ → μ₂.MutuallySingular ν₂