mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.OplaxFunctor B CategoryTheory.Cat}
  (η : CategoryTheory.Oplax.StrongTrans F G) {a b c : B} {a' : CategoryTheory.Cat} (f : a ⟶ b) (g : b ⟶ c)
  (h : G.obj c ⟶ a') (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp
      (h.toFunctor.map ((η.naturality (CategoryTheory.CategoryStruct.comp f g)).hom.toNatTrans.app X))
      (h.toFunctor.map ((G.mapComp f g).toNatTrans.app ((η.app a).toFunctor.obj X))) =
    CategoryTheory.CategoryStruct.comp (h.toFunctor.map ((η.app c).toFunctor.map ((F.mapComp f g).toNatTrans.app X)))
      (CategoryTheory.CategoryStruct.comp
        (h.toFunctor.map
          (CategoryTheory.CategoryStruct.id
            ((η.app c).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj X)))))
        (CategoryTheory.CategoryStruct.comp
          (h.toFunctor.map ((η.naturality g).hom.toNatTrans.app ((F.map f).toFunctor.obj X)))
          (CategoryTheory.CategoryStruct.comp
            (h.toFunctor.map
              (CategoryTheory.CategoryStruct.id
                ((G.map g).toFunctor.obj ((η.app b).toFunctor.obj ((F.map f).toFunctor.obj X)))))
            (CategoryTheory.CategoryStruct.comp
              (h.toFunctor.map ((G.map g).toFunctor.map ((η.naturality f).hom.toNatTrans.app X)))
              (h.toFunctor.map
                (CategoryTheory.CategoryStruct.id
                  ((G.map g).toFunctor.obj ((G.map f).toFunctor.obj ((η.app a).toFunctor.obj X)))))))))
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- The condition of `CreatesFiniteProducts` can be checked for finite types in an arbitrary
universe.  -/
CategoryTheory.Limits.CreatesFiniteProducts.mk' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          ((J : Type w) → [Fintype J] → CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete J) F) →
            CategoryTheory.Limits.CreatesFiniteProducts F
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.coimIsoIm_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Arrow C),
  CategoryTheory.Abelian.coimIsoIm.inv.app X = CategoryTheory.inv (CategoryTheory.Abelian.coimageImageComparison X.hom)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyData.mapOpcyclesIso_eq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (hr : S.RightHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S.HasRightHomology]
  [inst_6 : F.PreservesRightHomologyOf S], S.mapOpcyclesIso F = (hr.map F).opcyclesIso ≪≫ F.mapIso hr.opcyclesIso.symm
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.adj₁_counit_app_rightToLeft_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful]
  (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.adj₁.counit.app (H.obj X))
      (CategoryTheory.CategoryStruct.comp (t.rightToLeft.app X) h) =
    CategoryTheory.CategoryStruct.comp (F.map (t.adj₂.counit.app X)) h
-- Lean.Data.Options
Lean.OptionDecl.fullDescr : Lean.OptionDecl → String
-- Mathlib.Order.Lattice
inf_eq_iff_sup_eq : ∀ {α : Type u} [inst : Lattice α] {a b : α}, a ⊓ b = b ↔ a ⊔ b = a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfcₙ_lt_iff : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (c : NNReal),
  autoParam (ContinuousOn f (quasispectrum 𝕜 a)) nnnorm_cfcₙ_lt_iff._auto_1 →
    autoParam (f 0 = 0) nnnorm_cfcₙ_lt_iff._auto_3 →
      autoParam (p a) nnnorm_cfcₙ_lt_iff._auto_5 → (‖cfcₙ f a‖₊ < c ↔ ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖₊ < c)
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
/-- The projection on a summand of the coproduct decomposition given
by a splitting of a simplicial object.  -/
CategoryTheory.SimplicialObject.Splitting.πSummand : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      (s : X.Splitting) →
        [CategoryTheory.Limits.HasZeroMorphisms C] →
          {Δ : SimplexCategoryᵒᵖ} →
            (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) → X.obj Δ ⟶ s.N (Opposite.unop A.fst).len
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKey?_alter_eq_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.minKey? = some k ↔
    (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (compare k k').isLE = true
-- Aesop.Search.Expansion.Simp
Aesop.SimpResult.solved.inj : ∀ {usedTheorems usedTheorems_1 : Lean.Meta.Simp.UsedSimps},
  Aesop.SimpResult.solved usedTheorems = Aesop.SimpResult.solved usedTheorems_1 → usedTheorems = usedTheorems_1
-- Init.Core
Except.ok.injEq : ∀ {ε : Type u} {α : Type v} (a a_1 : α), (Except.ok a = Except.ok a_1) = (a = a_1)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.desc_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {V W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : V ⟶ W) (g : X ⟶ V) (h : Y ⟶ V),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc g h) f =
    CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp g f) (CategoryTheory.CategoryStruct.comp h f)
-- Mathlib.Topology.Perfect
Perfect.closure_nhds_inter : ∀ {α : Type u_1} [inst : TopologicalSpace α] {C U : Set α},
  Perfect C → ∀ x ∈ C, x ∈ U → IsOpen U → Perfect (closure (U ∩ C)) ∧ (closure (U ∩ C)).Nonempty
-- Mathlib.Analysis.ODE.Basic
isIntegralCurveAt_iff_exists_mem_nhds : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ : ℝ},
  IsIntegralCurveAt γ v t₀ ↔ ∃ s ∈ nhds t₀, IsIntegralCurveOn γ v s
-- Lean.Meta.LetToHave
/-- Enters a lambda/let/have telescope, checking that each domain type is a type.
For let/have, checks that each value has a type defeq to the domain type.
Calls `finalize` once the telescope is constructed.
 -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitLambdaLet.go : Lean.LocalContext → Array Lean.Expr → Lean.Expr → List Lean.FVarId → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_lt_norm_mul_iff_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F},
  inner ℝ x y < ‖x‖ * ‖y‖ ↔ ‖y‖ • x ≠ ‖x‖ • y
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.sum_integral_adjacent_intervals_Ico : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ}
  {a : ℕ → ℝ} {m n : ℕ},
  m ≤ n →
    (∀ k ∈ Set.Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))) →
      ∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a n, f x ∂μ
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS_ofNat : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (n : ℕ), preNormEDS b c d ↑n = preNormEDS' b c d n
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.PreSubmersivePresentation.ofHasCoeffs_relation : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] (P : Algebra.PreSubmersivePresentation R S ι σ) (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀] (r : σ),
  (P.ofHasCoeffs R₀).relation r = Algebra.Presentation.relationOfHasCoeffs R₀ r
-- Mathlib.RingTheory.Adjoin.Field
/-- If `K` and `L` are field extensions of `F` and we have `s : Finset K` such that
the minimal polynomial of each `x ∈ s` splits in `L` then `Algebra.adjoin F s` embeds in `L`.  -/
Polynomial.lift_of_splits : ∀ {F : Type u_2} {K : Type u_3} {L : Type u_4} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] (s : Finset K),
  (∀ x ∈ s, IsIntegral F x ∧ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) →
    Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
-- Init.Coe
CoeOTC.mk : {α : Sort u} → {β : Sort v} → (α → β) → CoeOTC α β
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instHasFiniteLimitsScheme : CategoryTheory.Limits.HasFiniteLimits AlgebraicGeometry.Scheme
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
arithGeom_eq' : ∀ {R : Type u_1} {a b u₀ : R} [inst : Field R],
  a ≠ 1 → arithGeom a b u₀ = fun n => a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)
-- Mathlib.FieldTheory.PrimeField
/-- The smallest subfield of a field of characteristic `p` is (the image of) `ZMod p`.
Note that the fact that the field `K` is of characteristic `p` is stated by the fact that it is
`ZMod p`-algebra.
 -/
Subfield.bot_eq_of_zMod_algebra : ∀ {K : Type u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] [inst : Field K] [inst_1 : Algebra (ZMod p) K],
  ⊥ = (algebraMap (ZMod p) K).fieldRange
-- Mathlib.Algebra.Quaternion
Quaternion.coe_intCast : ∀ {R : Type u_3} [inst : CommRing R] (z : ℤ), ↑↑z = ↑z
-- Mathlib.FieldTheory.Perfect
PerfectRing.ofFiniteOfIsReduced : ∀ (p : ℕ) (R : Type u_2) [inst : CommRing R] [ExpChar R p] [Finite R] [IsReduced R], PerfectRing R p
-- Lean.CoreM
Lean.Core.saveState : Lean.CoreM Lean.Core.SavedState
-- Mathlib.Topology.UniformSpace.Basic
inhabitedUniformSpace : {α : Type ua} → Inhabited (UniformSpace α)
-- Lean.Linter.UnusedVariables
/-- Collection of all `MetavarContext`s following the execution of a tactic. We trawl these
if needed to find additional `fvarUses`.  -/
Lean.Linter.UnusedVariables.References.assignments : Lean.Linter.UnusedVariables.References → Array (Lean.PersistentHashMap Lean.MVarId Lean.Expr)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
/-- An auxiliary map from `realSpace K` to `logSpace K` used to prove that `completeFamily` is
linearly independent, see `linearIndependent_completeFamily`.
 -/
NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace : {K : Type u_1} →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      NumberField.mixedEmbedding.realSpace K →ₗ[ℝ] { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ } → ℝ
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
HurwitzZeta.hurwitzZetaOdd_eq : ∀ (a : UnitAddCircle) (s : ℂ),
  HurwitzZeta.hurwitzZetaOdd a s = (HurwitzZeta.hurwitzZeta a s - HurwitzZeta.hurwitzZeta (-a) s) / 2
-- Init.Data.String.Defs
_private.Init.Data.String.Defs.0.String.intercalate.go : String → String → List String → String
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
/-- A (category-theoretically) small version of `FGModuleCat R`. This is used to prove that
`FGModuleCat R` is essentially small. For actual use, it might be recommended to use the canonical
`CategoryTheory.SmallModel` instead of this construction.  -/
FGModuleRepr : (R : Type u) → [Ring R] → Type u
-- Mathlib.Algebra.Group.Shrink
Shrink.instSemigroup : {α : Type u_2} → [inst : Small.{v, u_2} α] → [Semigroup α] → Semigroup (Shrink.{v, u_2} α)
-- Init.Data.Vector.Basic
Vector.findSomeRevM? : {m : Type u_1 → Type u_2} →
  {α : Type u_3} → {β : Type u_1} → {n : ℕ} → [Monad m] → (α → m (Option β)) → Vector α n → m (Option β)
-- Init.Data.Int.LemmasAux
Int.natCast_ne_zero : ∀ {n : ℕ}, ↑n ≠ 0 ↔ n ≠ 0
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_top_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E),
  ⊤.relfinrank A = 1
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.eq_toNNRealLinear_toRealPositiveLinear : ∀ {α : Type u_2} [inst : TopologicalSpace α] (Λ : CompactlySupportedContinuousMap α NNReal →ₗ[NNReal] NNReal),
  CompactlySupportedContinuousMap.toNNRealLinear (CompactlySupportedContinuousMap.toRealPositiveLinear Λ) = Λ
-- Batteries.Data.List.Lemmas
List.countPBefore_cons_zero : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {a : α}, List.countPBefore p (a :: xs) 0 = 0
-- Init.Data.UInt.Lemmas
USize.toBitVec_mul : ∀ {a b : USize}, (a * b).toBitVec = a.toBitVec * b.toBitVec
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extendedHom_coeIdeal_eq_map : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] (I : Ideal A), (FractionalIdeal.extendedHom L B) ↑I = ↑(Ideal.map (algebraMap A B) I)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v},
  p.IsPath → u ≠ v → s(v, u) ∉ p.edges → (p.toSubgraph.spanningCoe ⊔ SimpleGraph.edge v u).IsCycles
-- Std.Internal.Do.WP.Conjunctive
/-- `OptionT` lifts conjunctivity from its base monad.  -/
Std.Internal.Do.OptionT.instWPConjunctive : ∀ {m : Type u → Type v} {Pred : Type u} {EPred : Type z} {α : 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] [Std.Internal.Do.WPConjunctive (m (Option α)) (Option α) Pred EPred],
  Std.Internal.Do.WPConjunctive (OptionT m α) α Pred (EPost.Cons✝ Pred EPred)
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.LClause.mk.sizeOf_spec : ∀ (lits : Array ℤ) (expr : Lean.Expr) (depth : ℕ),
  sizeOf { lits := lits, expr := expr, depth := depth } = 1 + sizeOf lits + sizeOf expr + sizeOf depth
-- Mathlib.Topology.MetricSpace.Contracting
/-- The point provided by `ContractingWith.fixedPoint` is actually a fixed point.  -/
ContractingWith.fixedPoint_isFixedPt : ∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [inst_1 : Nonempty α]
  [inst_2 : CompleteSpace α], Function.IsFixedPt f (ContractingWith.fixedPoint f hf)
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.smulTower_repr : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [inst_6 : IsScalarTower R S A] {ι : Type u_5}
  {ι' : Type u_6} (b : Module.Basis ι R S) (c : Module.Basis ι' S A) (x : A) (ij : ι × ι'),
  ((b.smulTower c).repr x) ij = (b.repr ((c.repr x) ij.2)) ij.1
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.isUnit_iff_isRegular_of_mulOpposite : ∀ {R : Type u_1} [inst : Semiring R] [IsArtinianRing Rᵐᵒᵖ] {x : R}, IsUnit x ↔ IsRegular x
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
/-- If `F : J ⥤ C` is a functor that has a colimit and is such that for all `j`,
`F.obj j` satisfies a property `P`, then this structure expresses that `colimit F`
is indeed a colimit of objects satisfying `P`.  -/
CategoryTheory.ObjectProperty.ColimitOfShape.colimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {J : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} J] →
          (F : CategoryTheory.Functor J C) →
            [inst_2 : CategoryTheory.Limits.HasColimit F] →
              (∀ (j : J), P (F.obj j)) → P.ColimitOfShape J (CategoryTheory.Limits.colimit F)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_bij_ne_one : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (i : (a : ι) → a ∈ s → f a ≠ 1 → κ),
  (∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t) →
    (∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
        i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂) →
      (∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b) →
        (∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)) → ∏ x ∈ s, f x = ∏ x ∈ t, g x
-- Mathlib.Data.Nat.Digits.Defs
Nat.digit_sum_le : ∀ (p n : ℕ), (p.digits n).sum ≤ n
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.relevant : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m)
  (q :
    ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
            (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace),
  ¬HomogeneousIdeal.irrelevant 𝒜 ≤
      AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asHomogeneousIdeal f_deg hm q
-- Mathlib.Topology.IsLocalHomeomorph
/-- The inverse function of `localInverseAt x` coincides with `f`.  -/
IsLocalHomeomorph.localInverseAt_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : IsLocalHomeomorph f) (x : X), ↑(hf.localInverseAt x).symm = f
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.infty_notMem_range_coe : ∀ {X : Type u_1}, OnePoint.infty ∉ Set.range OnePoint.some
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
/-- Construct an edge labeling from a symmetric function on adjacent vertices.  -/
SimpleGraph.EdgeLabeling.mk : {V : Type u_1} →
  {G : SimpleGraph V} →
    {K : Type u_3} →
      (f : (x y : V) → G.Adj x y → K) → (∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H) → G.EdgeLabeling K
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsKleinFour.card_four : ∀ {G : Type u_1} {inst : Group G} [self : IsKleinFour G], Nat.card G = 4
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableOn.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
  DifferentiableOn 𝕜 c s → DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 (c • f) s
-- Mathlib.CategoryTheory.Subobject.Basic
/-- When `C` has pullbacks, a morphism `f : X ⟶ Y` induces a functor `Subobject Y ⥤ Subobject X`,
by pulling back a monomorphism along `f`.  -/
CategoryTheory.Subobject.pullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [CategoryTheory.Limits.HasPullbacks C] →
        (X ⟶ Y) → CategoryTheory.Functor (CategoryTheory.Subobject Y) (CategoryTheory.Subobject X)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_toArray_iff_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {v : β}, (k, v) ∈ t.toArray ↔ t[k]? = some v
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_mono : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R], Monotone Int.floor
-- Mathlib.Algebra.Group.Pi.Basic
Pi.divInvOneMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → DivInvOneMonoid (f i)],
  Pi.divInvOneMonoid = { toDivInvMonoid := Pi.divInvMonoid, inv_one := ⋯ }
-- Mathlib.Data.Set.Basic
Set.ssubset_of_ssubset_of_subset : ∀ {α : Type u} {s₁ s₂ s₃ : Set α}, s₁ ⊂ s₂ → s₂ ⊆ s₃ → s₁ ⊂ s₃
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.M : Type → Type
-- Mathlib.Topology.CompactOpen
/-- The family of constant maps: `Y → C(X, Y)` as a continuous map.  -/
ContinuousMap.const' : {X : Type u_2} → {Y : Type u_3} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(Y, C(X, Y))
-- Lean.Parser.Types
Lean.Parser.ParserContextCore.toInputContext : Lean.Parser.ParserContextCore → Lean.Parser.InputContext
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.getKeyD_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {k fallback : α}, m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.getKeyD k fallback = m₂.getKeyD k fallback
-- Mathlib.GroupTheory.Complement
/-- The collection of right transversals of a subgroup  -/
Subgroup.RightTransversal : {G : Type u_1} → [inst : Group G] → Subgroup G → Type (max 0 u_1)
-- Mathlib.CategoryTheory.Limits.Shapes.SingleObj
/-- The explicit quotient construction of the colimit of `J : SingleObj G ⥤ Type u` is
equivalent to the quotient of `J.obj (SingleObj.star G)` by the induced action.  -/
CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient : {G : Type v} →
  [inst : Group G] →
    (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)) →
      J.ColimitType ≃ MulAction.orbitRel.Quotient G (J.obj (CategoryTheory.SingleObj.star G))
-- Mathlib.GroupTheory.Index
AddSubgroup.card_dvd_of_surjective : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (f : G →+ G'),
  Function.Surjective ⇑f → Nat.card G' ∣ Nat.card G
-- Init.Data.Option.Lemmas
Option.bind_apply : ∀ {α : Type u_1} {x : Option α} {α_1 : Type u_1} {f : α → Option α_1}, x >>= f = x.bind f
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.BoundedFormula.freeVarFinset.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) →
      (x : ℕ) →
        (x_1 : L.BoundedFormula α x) →
          ((_n : ℕ) → motive _n FirstOrder.Language.BoundedFormula.falsum) →
            ((_n : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin _n)) → motive _n (FirstOrder.Language.BoundedFormula.equal t₁ t₂)) →
              ((_n l : ℕ) →
                  (_R : L.Relations l) →
                    (ts : Fin l → L.Term (α ⊕ Fin _n)) → motive _n (FirstOrder.Language.BoundedFormula.rel _R ts)) →
                ((_n : ℕ) → (f₁ f₂ : L.BoundedFormula α _n) → motive _n (f₁.imp f₂)) →
                  ((_n : ℕ) → (f : L.BoundedFormula α (_n + 1)) → motive _n f.all) → motive x x_1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.id_c_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C)
  (U : (TopologicalSpace.Opens ↑↑X)ᵒᵖ),
  (CategoryTheory.CategoryStruct.id X).c.app U = X.presheaf.map (CategoryTheory.CategoryStruct.id U)
-- Mathlib.Combinatorics.SimpleGraph.Sum
_private.Mathlib.Combinatorics.SimpleGraph.Sum.0.SimpleGraph.sum.match_1.splitter : {V : Type u_1} →
  {W : Type u_2} →
    (motive : V ⊕ W → V ⊕ W → Sort u_3) →
      (x x_1 : V ⊕ W) →
        ((u v : V) → motive (Sum.inl u) (Sum.inl v)) →
          ((u v : W) → motive (Sum.inr u) (Sum.inr v)) →
            ((x x_2 : V ⊕ W) →
                (∀ (u v : V), x = Sum.inl u → x_2 = Sum.inl v → False) →
                  (∀ (u v : W), x = Sum.inr u → x_2 = Sum.inr v → False) → motive x x_2) →
              motive x x_1
-- Init.Data.BitVec.Lemmas
BitVec.smtSDiv_zero : ∀ {n : ℕ} {x : BitVec n}, x.smtSDiv 0#n = if x.slt 0#n = true then 1#n else BitVec.allOnes n