mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
/-- The natural isomorphism `(K⟦n⟧).sc' i j k ≅ K.sc' i' j' k'` when `n + i = i'`,
`n + j = j'` and `n + k = k'`.  -/
CochainComplex.shiftShortComplexFunctor' : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (n i j k i' j' k' : ℤ) →
        n + i = i' →
          n + j = j' →
            n + k = k' →
              ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).comp
                  (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℤ) i j k) ≅
                HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℤ) i' j' k')
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.liftFromProjective_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) {P : C} (f : P ⟶ S.X₂) [inst_2 : CategoryTheory.Projective P]
  (hf : CategoryTheory.CategoryStruct.comp f S.g = 0) {Z : C} (h : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hS.liftFromProjective f hf) (CategoryTheory.CategoryStruct.comp S.f h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Order.Category.BddLat
BddLat.coe_forget_to_semilatSup : ∀ (X : BddLat), ((CategoryTheory.forget₂ BddLat SemilatSupCat).obj X).X = ↑X.toLat
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- The point of `S` below `x` and `y`.  -/
AlgebraicGeometry.Scheme.Pullback.Triplet.s : {X Y S : AlgebraicGeometry.Scheme} → {f : X ⟶ S} → {g : Y ⟶ S} → AlgebraicGeometry.Scheme.Pullback.Triplet f g → ↥S
-- Mathlib.Combinatorics.Graph.Simple
Graph.not_isLoopAt : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Loopless] (e : β) (x : α), ¬G.IsLoopAt e x
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivWithinAt_const_add_iff : ∀ {𝕜 : 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}
  {f' : E →L[𝕜] F} {x : E} {s : Set E} (c : F), HasFDerivWithinAt (fun x => c + f x) f' s x ↔ HasFDerivWithinAt f f' s x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_eq_getD_get? : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {a : α} {fallback : β},
      Std.DTreeMap.Internal.Impl.Const.getD t a fallback = (Std.DTreeMap.Internal.Impl.Const.get? t a).getD fallback
-- Init.Prelude
Fin.eq_of_val_eq : ∀ {n : ℕ} {i j : Fin n}, ↑i = ↑j → i = j
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.nestedBC.sizeOf_spec : sizeOf Lean.Elab.Term.Do.ToTerm.Kind.nestedBC = 1
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- For any homomorphism `φ` in a fiber `Fib S`, its image under `ι S` lies over `𝟙 S`.  -/
HasFibers.homLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] {S : 𝒮} {a b : HasFibers.Fib p S} (φ : a ⟶ b),
  p.IsHomLift (CategoryTheory.CategoryStruct.id S) ((HasFibers.ι S).map φ)
-- Mathlib.Algebra.Group.Hom.Defs
/-- `M →* N` is the type of functions `M → N` that preserve the `MulOne` structure.
`MonoidHom` is used for both monoid and group homomorphisms.

When possible, instead of parametrizing results over `(f : M →* N)`,
you should parametrize over `(F : Type*) [MonoidHomClass F M N] (f : F)`.

When you extend this structure, make sure to extend `MonoidHomClass`.


[Wikidata Q868169](https://www.wikidata.org/wiki/Q868169) -/
MonoidHom : (M : Type u_10) → (N : Type u_11) → [MulOne M] → [MulOne N] → Type (max u_10 u_11)
-- Mathlib.Topology.Algebra.Ring.Compact
IsLocalRing.isOpen_iff_finite_quotient : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R]
  [IsLocalRing R] [IsNoetherianRing R] {I : Ideal R}, IsOpen ↑I ↔ Finite (R ⧸ I)
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.zero_genWeightSpace_eq_top_of_nilpotent : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [LieModule.IsNilpotent L M], LieModule.genWeightSpace M 0 = ⊤
-- Mathlib.Algebra.Ring.Defs
instMulZeroClassOfSemiring : {α : Type u} → [Semiring α] → MulZeroClass α
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Biprod.unipotentUpper_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ : C} (r : X₁ ⟶ X₂),
  (CategoryTheory.Biprod.unipotentUpper r).hom =
    CategoryTheory.Biprod.ofComponents (CategoryTheory.CategoryStruct.id X₁) r 0 (CategoryTheory.CategoryStruct.id X₂)
-- Init.GrindInstances.ToInt
Lean.Grind.instLEInt32SintOfNatNat : Lean.Grind.ToInt.LE Int32 (Lean.Grind.IntInterval.sint 32)
-- Mathlib.Order.CompactlyGenerated.Basic
CompleteLattice.WellFoundedGT.isSupFiniteCompact : ∀ (α : Type u_2) [inst : CompleteLattice α] [WellFoundedGT α], CompleteLattice.IsSupFiniteCompact α
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.instHasInjectiveDimensionLTOfNatNatOfInjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C)
  [CategoryTheory.Injective X], CategoryTheory.HasInjectiveDimensionLT X 1
-- Lean.Parser.Command
Lean.Parser.Command.variable.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.ModelTheory.Satisfiability
/-- The **Upward Löwenheim–Skolem Theorem**: If `κ` is a cardinal greater than the cardinalities of
`L` and an infinite `L`-structure `M`, then `M` has an elementary extension of cardinality `κ`.  -/
FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_ge : ∀ (L : FirstOrder.Language) (M : Type w') [inst : L.Structure M] [iM : Infinite M] (κ : Cardinal.{w}),
  Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ →
    Cardinal.lift.{w, w'} (Cardinal.mk M) ≤ Cardinal.lift.{w', w} κ →
      ∃ N, Nonempty (L.ElementaryEmbedding M ↑N) ∧ Cardinal.mk ↑N = κ
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.DeclValue.extern.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (externAttrData : Lean.ExternAttrData),
  sizeOf (Lean.Compiler.LCNF.DeclValue.extern externAttrData) = 1 + sizeOf externAttrData
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.strongEpi_factorThruImage_of_strongEpiMonoFactorisation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] (F : CategoryTheory.Limits.StrongEpiMonoFactorisation f),
  CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- **Sturm bound for level-1 modular forms (natural weight).** If a modular form `f` of weight
`k : ℕ` has q-expansion of order strictly greater than `k / 12`, then `f` is identically zero.  -/
ModularForm.sturm_bound_levelOne_nat : ∀ {k : ℕ} {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k},
  ↑(k / 12) < (UpperHalfPlane.qExpansion 1 ⇑f).order → f = 0
-- Mathlib.Order.Compare
cmpLE_ofDual : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (x y : αᵒᵈ),
  cmpLE (OrderDual.ofDual x) (OrderDual.ofDual y) = cmpLE y x
-- Mathlib.Topology.PartialHomeomorph.Basic
Set.partialHomeomorphSubtypeCoe.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X) (hs : Nonempty ↑s),
  s.partialHomeomorphSubtypeCoe hs = Topology.IsEmbedding.toPartialHomeomorph Subtype.val ⋯
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
NNReal.eventually_pow_one_div_le : ∀ (x : NNReal) {y : NNReal}, 1 < y → ∀ᶠ (n : ℕ) in Filter.atTop, x ^ (1 / ↑n) ≤ y
-- Mathlib.CategoryTheory.PUnit
CategoryTheory.Functor.star_obj_as : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (x : C),
  ((CategoryTheory.Functor.star C).obj x).as = PUnit.unit
-- Mathlib.RingTheory.Localization.Integral
IsLocalization.integerNormalization_spec : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] (p : Polynomial S),
  ∃ b ∈ M, Polynomial.map (algebraMap R S) (IsLocalization.integerNormalization M p) = b • p
-- Init.Data.List.Lemmas
List.getLast_singleton : ∀ {α : Type u_1} {a : α} (h : [a] ≠ []), [a].getLast h = a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
IsStarNormal.instIsometricContinuousFunctionalCalculus : ∀ {A : Type u_1} [inst : CStarAlgebra A], IsometricContinuousFunctionalCalculus ℂ A IsStarNormal
-- Mathlib.Geometry.RingedSpace.SheafedSpace
/-- A sheafed space is a presheafed space which happens to be a sheaf.  -/
AlgebraicGeometry.SheafedSpace.IsSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : AlgebraicGeometry.SheafedSpace C),
  self.presheaf.IsSheaf
-- Mathlib.MeasureTheory.Group.FoelnerFilter
amenable_of_maxAddFoelner_neBot : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] [MeasureTheory.VAddInvariantMeasure G X μ] [(maxAddFoelner G μ).NeBot],
  ∃ m,
    m Set.univ = 1 ∧
      (∀ (s t : Set X), MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) ∧
        ∀ (g : G) (s : Set X), m (g +ᵥ s) = m s
-- Mathlib.Algebra.Group.ULift
ULift.zero_down : ∀ {α : Type u} [inst : Zero α], ULift.down 0 = 0
-- Mathlib.Data.Part
Part.some_append_some : ∀ {α : Type u_1} [inst : Append α] (a b : α), Part.some a ++ Part.some b = Part.some (a ++ b)
-- Mathlib.Order.Directed
/-- **Alias** of the forward direction of `directedOn_iff_isDirectedOrder`. -/
DirectedOn.isDirectedOrder : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, DirectedOn (fun x1 x2 => x1 ≤ x2) s → IsDirectedOrder ↑s
-- Batteries.CodeAction.Attr
Batteries.CodeAction.TacticCodeActions.mk.inj : ∀ {onAnyTactic : Array Batteries.CodeAction.TacticCodeAction}
  {onTactic : Lean.NameMap (Array Batteries.CodeAction.TacticCodeAction)}
  {onAnyTactic_1 : Array Batteries.CodeAction.TacticCodeAction}
  {onTactic_1 : Lean.NameMap (Array Batteries.CodeAction.TacticCodeAction)},
  { onAnyTactic := onAnyTactic, onTactic := onTactic } = { onAnyTactic := onAnyTactic_1, onTactic := onTactic_1 } →
    onAnyTactic = onAnyTactic_1 ∧ onTactic = onTactic_1
-- Mathlib.Order.Bounds.Basic
bddBelow_singleton : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, BddBelow {a}
-- Mathlib.Analysis.Normed.Ring.Basic
MulOpposite.instNonUnitalNormedRing : {α : Type u_2} → [NonUnitalNormedRing α] → NonUnitalNormedRing αᵐᵒᵖ
-- Init.Data.Array.Lemmas
Array.filterMap_flatMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {g : α → Array β} {f : β → Option γ},
  Array.filterMap f (Array.flatMap g xs) = Array.flatMap (fun a => Array.filterMap f (g a)) xs
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.toBitVec_minValueSealed_eq_intMinSealed : Int64.minValueSealed✝.toBitVec = BitVec.Signed.intMinSealed✝ 64
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- If `m` and `n` are finite and lie in the same universe, the rank of `m × n` matrices is
`(#n * #m).lift`.  -/
rank_matrix' : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] (m n : Type v) [Finite m] [Finite n],
  Module.rank R (Matrix m n R) = Cardinal.lift.{u, v} (Cardinal.mk m * Cardinal.mk n)
-- Mathlib.RingTheory.WittVector.Compare
/-- `toPadicInt` lifts `toZModPow : 𝕎 (ZMod p) →+* ZMod (p ^ k)` to a ring hom to `ℤ_[p]`
using `PadicInt.lift`, the universal property of `ℤ_[p]`.
 -/
WittVector.toPadicInt : (p : ℕ) → [hp : Fact (Nat.Prime p)] → WittVector p (ZMod p) →+* ℤ_[p]
-- Mathlib.RingTheory.Trace.Basic
Module.Basis.traceDual_repr_apply : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type w}
  [inst_3 : FiniteDimensional K L] [inst_4 : Algebra.IsSeparable K L] [inst_5 : Finite ι] [inst_6 : DecidableEq ι]
  (b : Module.Basis ι K L) (x : L) (i : ι), (b.traceDual.repr x) i = ((Algebra.traceForm K L) x) (b i)
-- Aesop.Util.Basic
Aesop.hasSorry : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.Expr → m Bool
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (root : Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex)
  (tries : Array (Lean.Meta.RefinedDiscrTree.Trie α)),
  sizeOf { root := root, tries := tries } = 1 + sizeOf root + sizeOf tries
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- Simultaneously swapping both the ordering of the applied duals and the ordering of the
tensor product argument preserves evaluation.  -/
TensorProduct.dualDistrib_apply_comm : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N]
  (w : TensorProduct R (Module.Dual R N) (Module.Dual R M)) (z : TensorProduct R M N),
  ((TensorProduct.dualDistrib R N M) w) ((TensorProduct.comm R M N) z) =
    ((TensorProduct.dualDistrib R M N) ((TensorProduct.comm R (Module.Dual R N) (Module.Dual R M)) w)) z
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.leadingCoeff.eq_1 : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] (x : HahnSeries Γ R),
  x.leadingCoeff = WithTop.recTopCoe 0 x.coeff x.orderTop
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.apply_smulCommClass' : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : SMul S R] [inst_4 : SMul S M] [IsScalarTower S R M], SMulCommClass (Module.End R M) S M
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Result.addLambdas : Lean.Meta.Simp.Result → Array Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.isHomogeneous_iff_forall_subset : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  (I : Ideal A), Ideal.IsHomogeneous 𝒜 I ↔ ∀ (i : ι), ↑I ⊆ ⇑(GradedRing.proj 𝒜 i) ⁻¹' ↑I
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidSearchFrom.below.matched : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {motive :
    (a : s.Pos) →
      (a_1 : List (String.Slice.Pattern.SearchStep s)) → String.Slice.Pattern.Model.IsValidSearchFrom pat a a_1 → Prop}
  {l : List (String.Slice.Pattern.SearchStep s)} {startPos endPos : s.Pos}
  (a : String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos)
  (a_1 : String.Slice.Pattern.Model.IsValidSearchFrom pat endPos l),
  String.Slice.Pattern.Model.IsValidSearchFrom.below a_1 →
    motive endPos l a_1 → String.Slice.Pattern.Model.IsValidSearchFrom.below ⋯
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.card_le_chromaticNumber_iff_forall_surjective : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} [inst : Fintype α],
  ↑(Fintype.card α) ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring α), Function.Surjective ⇑C
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
_private.Mathlib.Data.QPF.Multivariate.Constructions.Sigma.0.MvQPF.Sigma.instMvFunctor.match_1.eq_1 : ∀ {n : ℕ} {A : Type u_1} (F : A → TypeVec.{u_1} n → Type u_1) {α : TypeVec.{u_1} n}
  (motive : MvQPF.Sigma F α → Sort u_2) (a : A) (x : F a α) (h_1 : (a : A) → (x : F a α) → motive ⟨a, x⟩),
  (match ⟨a, x⟩ with
    | ⟨a, x⟩ => h_1 a x) =
    h_1 a x
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rcc_succ_right_eq_push : ∀ {m n : ℤ}, m ≤ n + 1 → (m...=n + 1).toArray = (m...=n).toArray.push (n + 1)
-- Mathlib.Algebra.Ring.Prod
RingEquiv.prodProdProdComm_toMulEquiv : ∀ (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [inst : NonAssocSemiring R]
  [inst_1 : NonAssocSemiring S] [inst_2 : NonAssocSemiring R'] [inst_3 : NonAssocSemiring S'],
  ↑(RingEquiv.prodProdProdComm R R' S S') = MulEquiv.prodProdProdComm R R' S S'
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
/-- The sheaf condition in terms of unique gluings. A presheaf `F : Presheaf C X` satisfies this sheaf
condition if and only if, for every compatible family of sections `sf : Π i : ι, F.obj (op (U i))`,
there exists a unique gluing `s : F.obj (op (iSup U))`.

We prove this to be equivalent to the usual one below in
`TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing`
 -/
TopCat.Presheaf.IsSheafUniqueGluing : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {FC : C → C → Type u_2} →
      {CC : C → Type u_3} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [CategoryTheory.ConcreteCategory C FC] → {X : TopCat} → TopCat.Presheaf C X → Prop
-- Mathlib.SetTheory.Ordinal.Univ
Ordinal.liftPrincipalSeg_coe : ⇑Ordinal.liftPrincipalSeg.toRelEmbedding = Ordinal.lift.{max (u + 1) v, u}
-- Mathlib.RingTheory.Coprime.Lemmas
IsRelPrime.of_prod_right : ∀ {α : Type u_1} {I : Type u_2} [inst : CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I},
  IsRelPrime x (∏ i ∈ t, s i) → ∀ i ∈ t, IsRelPrime x (s i)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.endsWith_char_eq_false_iff_get : ∀ {c : Char} {s : String.Slice}, s.endsWith c = false ↔ ∀ (h : s.endPos ≠ s.startPos), (s.endPos.prev h).get ⋯ ≠ c
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceShiftLeft : Lean.Meta.Simp.DSimproc
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- Substitution of power series into a power series, as an `AlgHom`.  -/
PowerSeries.substAlgHom : {R : Type u_2} →
  [inst : CommRing R] →
    {τ : Type u_3} →
      {S : Type u_4} →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {a : MvPowerSeries τ S} → PowerSeries.HasSubst a → PowerSeries R →ₐ[R] MvPowerSeries τ S
-- Mathlib.Order.Lattice
Pi.instMinForall_mathlib.eq_1 : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Min (α' i)],
  Pi.instMinForall_mathlib = { min := fun f g i => f i ⊓ g i }
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- A def to put an `Mul` instance on a type with a `Language.ring.Structure` instance.

To be used sparingly, usually only when defining a more useful definition like,
`[Language.ring.Structure K] -> [Theory.field.Model K] -> Field K`  -/
FirstOrder.Ring.mulOfRingStructure : (R : Type u_2) → [FirstOrder.Language.ring.Structure R] → Mul R
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.instBot : {α : Type u_1} → [inst : CompleteLattice α] → {L : CompleteSublattice α} → Bot ↥L
-- Mathlib.Data.Nat.PSub
Nat.psub_succ : ∀ {m n : ℕ}, m.psub n.succ = m.psub n >>= Nat.ppred
-- Mathlib.NumberTheory.NumberField.Basic
/-- The kernel of the algebraMap between ring of integers is `⊥`.  -/
NumberField.RingOfIntegers.ker_algebraMap_eq_bot : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  RingHom.ker (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) = ⊥
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.ExactPairing.evaluation_coevaluation'' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  [inst_2 : CategoryTheory.ExactPairing X Y],
  CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (η_ X Y) X)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (ε_ X Y)) =
    CategoryTheory.MonoidalCoherence.iso.hom
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mrange_inr' : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.mrange (MonoidHom.inr M N) = Submonoid.comap (MonoidHom.fst M N) ⊥
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The sine of the angle between two vectors is 1 if and only if the angle is π / 2.  -/
InnerProductGeometry.sin_eq_one_iff_angle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  Real.sin (InnerProductGeometry.angle x y) = 1 ↔ InnerProductGeometry.angle x y = Real.pi / 2
-- Init.Data.String.Lemmas.Intercalate
String.intercalate_cons_append : ∀ {s t u : String} {l : List String}, s.intercalate ((t ++ u) :: l) = t ++ s.intercalate (u :: l)
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.OfLocalizationSpan.and : ∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => Q) →
      RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] f => P f ∧ Q f
-- Lean.DocString.Parser
/-- Succeeds when the parser is looking at an unordered list indicator.
 -/
Lean.Doc.Parser.lookaheadUnorderedListIndicator : Lean.Doc.Parser.BlockCtxt → (Lean.Doc.Parser.UnorderedListType → Lean.Parser.ParserFn) → Lean.Parser.ParserFn
-- Mathlib.Analysis.Complex.Hadamard
/-- The function `invInterpStrip` is `diffContOnCl`.  -/
Complex.HadamardThreeLines.diffContOnCl_invInterpStrip : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) {ε : ℝ},
  ε > 0 →
    DiffContOnCl ℂ (fun z => Complex.HadamardThreeLines.invInterpStrip f z ε)
      (Complex.HadamardThreeLines.verticalStrip 0 1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  (t.erase k).getKeyD k fallback = fallback
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis.0.Tactic.ComputeAsymptotics.BasisExtension.getBasis.match_1.eq_2 : ∀ (motive : (basis : Tactic.ComputeAsymptotics.Basis) → Tactic.ComputeAsymptotics.BasisExtension basis → Sort u_1)
  (basis_hd : ℝ → ℝ) (basis_tl : Tactic.ComputeAsymptotics.Basis)
  (ex : Tactic.ComputeAsymptotics.BasisExtension basis_tl)
  (h_1 : Unit → motive [] Tactic.ComputeAsymptotics.BasisExtension.nil)
  (h_2 :
    (basis_hd : ℝ → ℝ) →
      (basis_tl : Tactic.ComputeAsymptotics.Basis) →
        (ex : Tactic.ComputeAsymptotics.BasisExtension basis_tl) →
          motive (basis_hd :: basis_tl) (Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex))
  (h_3 :
    (basis : Tactic.ComputeAsymptotics.Basis) →
      (f : ℝ → ℝ) →
        (ex : Tactic.ComputeAsymptotics.BasisExtension basis) →
          motive basis (Tactic.ComputeAsymptotics.BasisExtension.insert f ex)),
  (match basis_hd :: basis_tl, Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex with
    | .([]), Tactic.ComputeAsymptotics.BasisExtension.nil => h_1 ()
    | .(basis_hd :: basis_tl), Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex => h_2 basis_hd basis_tl ex
    | basis, Tactic.ComputeAsymptotics.BasisExtension.insert f ex => h_3 basis f ex) =
    h_2 basis_hd basis_tl ex
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.add_le_of_lt : ∀ {m a b : ℕ}, a ≡ b [MOD m] → a < b → a + m ≤ b
-- Lean.Server.Rpc.Basic
/-- `WithRpcRef α` marks values that RPC clients should see as opaque references.
This includes heavy objects such as `Lean.Environment`s
and non-serializable objects such as closures.

In the Lean server, `WithRpcRef α` is a structure containing a value of type `α`
and an associated `id`.
In an RPC client (e.g. the infoview), it is an opaque reference.
Thus, `WithRpcRef α` is cheap to transmit, but its data may only be accessed server-side.
In practice, this is used by client code to pass data
between various RPC methods provided by the server.

Two `WithRpcRef`s with the same `id` will yield the same client-side reference.

See also the docstring for `RpcEncodable`.
 -/
Lean.Server.WithRpcRef : Type u → Type u
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instInhabited : Inhabited CommGrpCat
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.IsPrincipal.span_singleton_generator : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Submodule R M)
  [inst_3 : S.IsPrincipal], R ∙ Submodule.IsPrincipal.generator S = S