mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both summable then so is the
`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position).  -/
Summable.int_rec : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] {f g : ℕ → M},
  Summable f → Summable g → Summable fun t => Int.rec f g t
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.toAddMonoidHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (h : M ≃+ N),
  h.toAddMonoidHom = { toFun := h.toFun, map_zero' := ⋯, map_add' := ⋯ }
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.anyM.eq_def : ∀ {m : Type → Type u} [inst : Monad m] {α : Type v} (p : α → m Bool) (x : List α),
  List.anyM p x =
    match x with
    | [] => pure false
    | a :: as => do
      let __do_lift ← p a
      match __do_lift with
        | true => pure true
        | false => List.anyM p as
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nnnorm_eq_of_L2 : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp 2 β),
  ‖x‖₊ = NNReal.sqrt (∑ i, ‖x.ofLp i‖₊ ^ 2)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.snd.eq_1 : ∀ (M : Type u_1) (α : Type u_2) (β : Type u_3) [inst : SMul M α] [inst_1 : SMul M β],
  MulActionHom.snd M α β = { toFun := Prod.snd, map_smul' := ⋯ }
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.eventually : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s t : Set α},
  Absorbs M s t → ∀ᶠ (a : M) in Bornology.cobounded M, t ⊆ a • s
-- Mathlib.Data.Bool.Count
List.count_true_add_count_false : ∀ (l : List Bool), List.count true l + List.count false l = l.length
-- Mathlib.Data.Nat.Digits.Lemmas
/-- The bijection `Nat.bijOn_ofDigits` stated as a bijection between `Finset`.
This spelling can be helpful for some proofs.
 -/
Nat.bijOn_ofDigits' : ∀ {b : ℕ} (hb : 1 < b) (l : ℕ), Set.BijOn (Nat.ofDigits b) ↑(List.fixedLengthDigits hb l) ↑(Finset.range (b ^ l))
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_multiset_singleton : ∀ {ι : Type u_1} (s : Finset ι), ∑ a ∈ s, {a} = s.val
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_inclusion : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S T : NonUnitalSubalgebra R A} (h : S ≤ T) (s : ↥S), ↑((NonUnitalSubalgebra.inclusion h) s) = ↑s
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Functoriality of `YonedaCollection F X` in `F`.  -/
CategoryTheory.OverPresheafAux.YonedaCollection.map₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} →
        {X : C} →
          {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} →
            (F ⟶ G) →
              CategoryTheory.OverPresheafAux.YonedaCollection F X → CategoryTheory.OverPresheafAux.YonedaCollection G X
-- Init.System.IO
/-- Acquires an exclusive or shared lock on the handle. Blocks to wait for the lock if necessary.

Acquiring an exclusive lock while already possessing a shared lock will **not** reliably succeed: it
works on Unix-like systems but not on Windows.
 -/
IO.FS.Handle.lock : IO.FS.Handle → optParam Bool true → IO Unit
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.map_one : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f), hf.map hf 1 1 = 1
-- Mathlib.Data.Finset.Prod
Finset.Nonempty.product : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, s.Nonempty → t.Nonempty → (s ×ˢ t).Nonempty
-- Lean.Expr
/-- Returns `p ↔ q`  -/
Lean.mkIff : Lean.Expr → Lean.Expr → Lean.Expr
-- Batteries.Data.Array.Merge
_private.Batteries.Data.Array.Merge.0.Array.mergeDedupWith.go.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.gt) → (Unit → motive Ordering.eq) → motive x
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_mul_X : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (s : σ) (p : MvPolynomial σ R),
  (p * MvPolynomial.X s).support = Finset.map (addRightEmbedding fun₀ | s => 1) p.support
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B],
  Algebra.TensorProduct.includeLeftRingHom.comp (algebraMap R A) =
    Algebra.TensorProduct.includeRight.comp (algebraMap R B)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.regular_neg_iff : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G], μ.neg.Regular ↔ μ.Regular
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instIsScalarTower' : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : CommSemiring R] [inst_4 : IsTopologicalSemiring R] {M : Type u_3} [inst_5 : SMulZeroClass M R]
  [IsScalarTower M R R] [inst_7 : ContinuousConstSMul M R],
  IsScalarTower M (ContinuousMapZero X R) (ContinuousMapZero X R)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftZero' : ∀ {C : Type u} (A : Type u_1) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (X Y : C) (f : X ⟶ Y),
  (CategoryTheory.shiftFunctor C 0).map f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftZero A X).hom
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.shiftZero A Y).inv)
-- Mathlib.Data.Fintype.EquivFin
Equiv.ofLeftInverseOfCardLE_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (hβα : Fintype.card β ≤ Fintype.card α)
  (f : α → β) (g : β → α) (h : Function.LeftInverse g f) (a : β), (Equiv.ofLeftInverseOfCardLE hβα f g h).symm a = g a
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.piFan_pt : ∀ {ι : Type u} (R : ι → CommRingCat), (CommRingCat.piFan R).pt = CommRingCat.of ((i : ι) → ↑(R i))
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.instRingConeClass : ∀ (R : Type u_1) [inst : Ring R], RingConeClass (RingCone R) R
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Transport an `IsKernel` across isomorphisms.  -/
CategoryTheory.Limits.IsKernel.ofIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          {X' Y' : C} →
            {f' : X' ⟶ Y'} →
              {s : CategoryTheory.Limits.KernelFork f} →
                CategoryTheory.Limits.IsLimit s →
                  (s' : CategoryTheory.Limits.KernelFork f') →
                    (eX : X ≅ X') →
                      (eY : Y ≅ Y') →
                        (e : s.pt ≅ s'.pt) →
                          CategoryTheory.CategoryStruct.comp eX.hom f' = CategoryTheory.CategoryStruct.comp f eY.hom →
                            CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.Limits.Fork.ι s') =
                                CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι s) eX.hom →
                              CategoryTheory.Limits.IsLimit s'
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderivWithin_comp_of_preimage_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M' → M} {g : M → 𝕜} {u : Set M}
  {s : Set M'} (x : M'),
  MDiffAt[u] g (f x) →
    MDiffAt[s] f x → f ⁻¹' u ∈ nhdsWithin x s → UniqueMDiffAt[s] x → d[s] (g ∘ f) x = d[u] g (f x) ∘SL mfderiv[s] f x
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a measure is a product of
characteristic functions if and only if it is a product measure.
This is the version for Hilbert spaces, see `charFunDual_eq_prod_iff`
for the Banach space version.  -/
MeasureTheory.charFun_eq_prod_iff : ∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] {mE : MeasurableSpace E} {mF : MeasurableSpace F}
  [CompleteSpace E] [CompleteSpace F] [SecondCountableTopology E] [SecondCountableTopology F] [BorelSpace E]
  [BorelSpace F] {μ : MeasureTheory.Measure E} {ν : MeasureTheory.Measure F} {ξ : MeasureTheory.Measure (E × F)}
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ξ],
  (∀ (t : WithLp 2 (E × F)),
      MeasureTheory.charFun (MeasureTheory.Measure.map (WithLp.toLp 2) ξ) t =
        MeasureTheory.charFun μ t.ofLp.1 * MeasureTheory.charFun ν t.ofLp.2) ↔
    ξ = μ.prod ν
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.sdiff_empty : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis s → TopologicalSpace.IsTopologicalBasis (s \ {∅})
-- Mathlib.Analysis.Convex.Combination
convexHull_prod : ∀ {R : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : LinearOrder R] [IsStrictOrderedRing R] (s : Set E) (t : Set F),
  (convexHull R) (s ×ˢ t) = (convexHull R) s ×ˢ (convexHull R) t
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearEquiv.conjContinuousAlgEquiv_refl : ∀ {𝕜 : Type u_1} {G : Type u_4} [inst : AddCommGroup G] [inst_1 : NormedField 𝕜] [inst_2 : Module 𝕜 G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalAddGroup G] [inst_5 : ContinuousConstSMul 𝕜 G],
  (ContinuousLinearEquiv.refl 𝕜 G).conjContinuousAlgEquiv = ContinuousAlgEquiv.refl 𝕜 (G →L[𝕜] G)
-- Lean.Meta.Tactic.Grind.Action
Lean.Meta.Grind.Action.TGrindStep.getTactic : Lean.Meta.Grind.TGrindStep → Lean.Meta.Grind.TGrind
-- Mathlib.Algebra.Group.Units.Defs
Units.instInv.eq_1 : ∀ {α : Type u} [inst : Monoid α],
  Units.instInv = { inv := fun u => { val := u.inv, inv := ↑u, val_inv := ⋯, inv_val := ⋯ } }
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- `a / b := a * b⁻¹`  -/
LinearOrderedCommGroupWithZero.div_eq_mul_inv : ∀ {α : Type u_3} [self : LinearOrderedCommGroupWithZero α] (a b : α), a / b = a * b⁻¹
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The equivalence between the nonsingular points on a Weierstrass curve `W` in affine coordinates
satisfying a predicate and the set of pairs `⟨x, y⟩` satisfying `W.Nonsingular x y` with zero.  -/
WeierstrassCurve.Affine.nonsingularPointEquivSubtype : {R : Type r} →
  [inst : CommRing R] →
    {W' : WeierstrassCurve.Affine R} →
      {p : W'.Point → Prop} →
        p WeierstrassCurve.Affine.Point.zero →
          { P // p P } ≃
            WithZero { xy // ∃ (h : W'.Nonsingular xy.1 xy.2), p (WeierstrassCurve.Affine.Point.some xy.1 xy.2 h) }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_eq_pi : ∀ {x : ℝ}, Real.arccos x = Real.pi ↔ x ≤ -1
-- Lean.Meta.CoeAttr
/-- The different types of coercions that are supported by the `coe` attribute.  -/
Lean.Meta.CoeFnType : Type
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.beq_iff_equiv : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [LawfulBEq α] [inst_3 : BEq β] [LawfulBEq β],
  (↑m₁).WF → (↑m₂).WF → (Std.DHashMap.Internal.Raw₀.Const.beq m₁ m₂ = true ↔ (↑m₁).Equiv ↑m₂)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.neg_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') (m : ι → M), (-g) m = -g m
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C)
  (X_1 : CategoryTheory.WithInitial SimplexCategory),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.unitIso.inv.app X).app X_1 =
    (match X_1 with
      | CategoryTheory.WithInitial.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithInitial.incl.comp X)).app x
      | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithInitial.star)).inv
-- Mathlib.Data.List.Sigma
List.nil_kunion : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {l : List (Sigma β)}, [].kunion l = l
-- Mathlib.Data.Vector.Basic
List.Vector.eraseIdx_insertIdx_self : ∀ {α : Type u_1} {n : ℕ} {a : α} {v : List.Vector α n} {i : Fin (n + 1)},
  List.Vector.eraseIdx i (List.Vector.insertIdx a i v) = v
-- Lean.Server.CodeActions.Basic
Lean.Server.instFromJsonCodeActionResolveData : Lean.FromJson Lean.Server.CodeActionResolveData
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.toAlgHom_ofComp_localizationAway : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) {T : Type u_7} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T],
  ((Algebra.Generators.localizationAway T g).ofComp P).toAlgHom
      ((MvPolynomial.rename Sum.inr) (P.σ g) * MvPolynomial.X (Sum.inl ()) - 1) =
    MvPolynomial.C g * MvPolynomial.X () - 1
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_eq_empty_iff_subset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s \ t = ∅ ↔ s ⊆ t
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_add_C : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R}, 0 < p.degree → (p + Polynomial.C a).degree = p.degree
-- Mathlib.Order.Nucleus
Nucleus.top_apply : ∀ {X : Type u_1} [inst : SemilatticeInf X] [inst_1 : OrderTop X] (x : X), ⊤ x = ⊤
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.startsWith_bool_eq_head? : ∀ {p : Char → Bool} {s : String}, s.startsWith p = Option.any p s.toList.head?
-- Mathlib.Order.SupClosed
infClosure_singleton : ∀ {α : Type u_3} [inst : SemilatticeInf α] {a : α}, infClosure {a} = {a}
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
SSet.chainComplex_hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] {X : SSet} {R : C} {n : ℕ} {T : C} {f g : (X.chainComplex R).X n ⟶ T},
  f = g ↔
    ∀ (x : X.obj (Opposite.op { len := n })),
      CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) f =
        CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) g
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.const.eq_def : ∀ (x : ℕ),
  Nat.Partrec.Code.const x =
    match x with
    | 0 => Nat.Partrec.Code.zero
    | n.succ => Nat.Partrec.Code.succ.comp (Nat.Partrec.Code.const n)
-- Mathlib.NumberTheory.Rayleigh
/-- Let `r` be an irrational number. Then `B⁺_r` and `B⁺'_r` are equal.  -/
Irrational.beattySeq'_pos_eq : ∀ {r : ℝ}, Irrational r → {x | ∃ k > 0, beattySeq' r k = x} = {x | ∃ k > 0, beattySeq r k = x}
-- Batteries.Data.List.Basic
/-- `Subperm l₁ l₂`, denoted `l₁ <+~ l₂`, means that `l₁` is a sublist of
a permutation of `l₂`. This is an analogue of `l₁ ⊆ l₂` which respects
multiplicities of elements, and is used for the `≤` relation on multisets.
 -/
List.Subperm : {α : Type u_1} → List α → List α → Prop
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.coe_fn_coe' : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  (f : A →ₑ*[φ] B), ⇑↑f = ⇑f
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.nonempty_fullyFaithful_iff : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁]
  [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂]
  (G : CategoryTheory.Functor D₁ D₂) [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] {D₁' : Type u₄'} {D₂' : Type u₅'}
  [inst_7 : CategoryTheory.Category.{v₄', u₄'} D₁'] [inst_8 : CategoryTheory.Category.{v₅', u₅'} D₂']
  (L₁' : CategoryTheory.Functor C₁ D₁') (L₂' : CategoryTheory.Functor C₂ D₂') [L₁'.IsLocalization W₁]
  [L₂'.IsLocalization W₂] (G' : CategoryTheory.Functor D₁' D₂') [CategoryTheory.CatCommSq Φ.functor L₁' L₂' G'],
  Nonempty G.FullyFaithful ↔ Nonempty G'.FullyFaithful
-- Mathlib.Order.Hom.CompleteLattice
/-- `FrameHomClass F α β` states that `F` is a type of frame morphisms. They preserve `⊓` and `⨆`.

You should extend this class when you extend `FrameHom`.  -/
FrameHomClass : (F : Type u_8) → (α : Type u_9) → (β : Type u_10) → [CompleteLattice α] → [CompleteLattice β] → [FunLike F α β] → Prop
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_maxKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {fallback : α} {he : Std.Internal.List.containsKey (Std.Internal.List.maxKeyD l fallback) l = true},
      Std.Internal.List.getKey (Std.Internal.List.maxKeyD l fallback) l he = Std.Internal.List.maxKeyD l fallback
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
returning `none` if no such key exists.
 -/
Std.ExtTreeMap.getKeyGT? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → Option α
-- Mathlib.Algebra.Homology.Homotopy
/-- An auxiliary construction for `mkInductive`.
 -/
Homotopy.mkCoinductiveAux₂ : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {P Q : CochainComplex V ℕ} →
        (e : P ⟶ Q) →
          (zero : P.X 1 ⟶ Q.X 0) →
            e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero →
              (one : P.X 2 ⟶ Q.X 1) →
                e.f 1 =
                    CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) +
                      CategoryTheory.CategoryStruct.comp (P.d 1 2) one →
                  ((n : ℕ) →
                      (p :
                          (f : P.X (n + 1) ⟶ Q.X n) ×'
                            (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
                              e.f (n + 1) =
                                CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                                  CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') →
                        (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
                          e.f (n + 2) =
                            CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) +
                              CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') →
                    (n : ℕ) →
                      (f : P.X n ⟶ HomologicalComplex.xPrev Q n) ×'
                        (f' : HomologicalComplex.xNext P n ⟶ Q.X n) ×'
                          e.f n =
                            CategoryTheory.CategoryStruct.comp f (HomologicalComplex.dTo Q n) +
                              CategoryTheory.CategoryStruct.comp (HomologicalComplex.dFrom P n) f'
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_rco_eq_some : ∀ {m n : ℤ} {i : ℕ}, i < (n - m).toNat → (m...n).toArray[i]? = some (m + ↑i)
-- Mathlib.Algebra.Order.Module.Defs
smul_neg_of_pos_of_neg : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [PosSMulStrictMono α β], 0 < a → b < 0 → a • b < 0
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
/-- Change the index category for `ObjectProperty.LimitOfShape`.  -/
CategoryTheory.ObjectProperty.LimitOfShape.reindex : {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] →
          {J' : Type u''} →
            [inst_2 : CategoryTheory.Category.{v'', u''} J'] →
              {X : C} → P.LimitOfShape J X → (G : CategoryTheory.Functor J' J) → [G.Initial] → P.LimitOfShape J' X
-- Mathlib.Topology.EMetricSpace.Defs
Metric.eball_mem_nhds : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α) {ε : ENNReal}, 0 < ε → Metric.eball x ε ∈ nhds x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- Given that the bottom square is a pullback, the pasted square is a pullback iff the top
square is.  -/
CategoryTheory.Limits.pasteVertIsPullbackEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ : C} →
      {f₁ : X₂ ⟶ X₁} →
        {f₂ : X₃ ⟶ X₂} →
          {i₁ : Y₁ ⟶ X₁} →
            {t₁ : CategoryTheory.Limits.PullbackCone i₁ f₁} →
              {i₂ : t₁.pt ⟶ X₂} →
                (t₂ : CategoryTheory.Limits.PullbackCone i₂ f₂) →
                  (hi₂ : i₂ = t₁.snd) →
                    CategoryTheory.Limits.IsLimit t₁ →
                      CategoryTheory.Limits.IsLimit (t₁.pasteVert t₂ hi₂) ≃ CategoryTheory.Limits.IsLimit t₂
-- Mathlib.Algebra.Group.Action.Defs
smulCommClass_self : ∀ (M : Type u_9) (α : Type u_10) [inst : CommMonoid M] [inst_1 : MulAction M α], SMulCommClass M M α
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mapAlgebra_apply : ∀ (R : Type u) [inst : CommSemiring R] (A : Type u_5) [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (M : CommRing.Pic R), (CommRing.Pic.mapAlgebra R A) M = CommRing.Pic.mk A (TensorProduct R A M.AsModule)
-- Lean.Expr
Lean.Int.mkInstSub : Lean.Expr
-- Init.Data.UInt.Lemmas
UInt64.two_mul : ∀ {a : UInt64}, 2 * a = a + a
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_concat_of_lt : ∀ {w n acc : ℕ} {x : BitVec w} {b : Bool}, 0 < n → (x.concat b).cpopNatRec n acc = b.toNat + x.cpopNatRec (n - 1) acc
-- Mathlib.Algebra.Star.Subalgebra
StarAlgHom.restrictScalars_apply : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  [inst_11 : Star A] [inst_12 : Star B] (f : A →⋆ₐ[S] B) (a : A), (StarAlgHom.restrictScalars R f) a = f a
-- Mathlib.Order.SuccPred.CompleteLinearOrder
exists_eq_ciInf_of_not_isPredPrelimit : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α},
  BddBelow (Set.range f) → ¬Order.IsPredPrelimit (⨅ i, f i) → ∃ i, f i = ⨅ i, f i