mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Monotone.Basic
strictMono_comp_ofDual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono (f ∘ ⇑OrderDual.ofDual) ↔ StrictAnti f
-- Std.Http.Data.Headers.Basic
/-- Returns `true` if the transfer encoding ends with chunked.
 -/
Std.Http.Header.TransferEncoding.isChunked : Std.Http.Header.TransferEncoding → Bool
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesOpIso_inv_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology]
  {Z : Cᵒᵖ} (h : S₁.op.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ).op
      (CategoryTheory.CategoryStruct.comp S₁.opcyclesOpIso.inv h) =
    CategoryTheory.CategoryStruct.comp S₂.opcyclesOpIso.inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ShortComplex.opcyclesMap (CategoryTheory.ShortComplex.opMap φ)) h)
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- Let `G` be a Type with addition.  `UniqueSums G` asserts that any two non-empty
finite subsets of `G` have the `UniqueAdd` property, with respect to some element of their
sum `A + B`.  -/
UniqueSums : (G : Type u_1) → [Add G] → Prop
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroMod.eq_1 : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type v} [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℕ),
  v.valuationOfNeZeroMod n =
    (AddEquiv.toMultiplicative (Int.quotientZMultiplesNatEquivZMod n)).toMonoidHom.comp
      (QuotientGroup.map (powMonoidHom n).range (AddSubgroup.toSubgroup (AddSubgroup.zmultiples ↑n)) v.valuationOfNeZero
        ⋯)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.isLittleO_const_logb_atTop : ∀ {b c : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → (fun x => c) =o[Filter.atTop] Real.logb b
-- Init.Data.String.Basic
String.Pos.next_le_of_lt : ∀ {s : String} {p q : s.Pos} {h : p ≠ s.endPos}, p < q → p.next h ≤ q
-- Mathlib.Algebra.Order.Group.PosPart
one_le_oneLePart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] (a : α), 1 ≤ a⁺ᵐ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCompletionOptions.toJson : Lean.Lsp.CompletionOptions → Lean.Json
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.descFunLift.eq_3 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (s : CategoryTheory.Limits.Cocone F), RingCat.Colimits.descFunLift F s RingCat.Colimits.Prequotient.one = 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.compare_minKey!_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : β → β}, cmp (Std.ExtDTreeMap.Const.modify t k f).minKey! t.minKey! = Ordering.eq
-- Mathlib.SetTheory.Lists
/-- Appending a ZFA list to a proper ZFA prelist.  -/
Lists'.cons : {α : Type u_1} → Lists α → Lists' α true → Lists' α true
-- Mathlib.Order.Filter.Prod
Filter.Eventually.prod_inl : ∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {p : α → Prop},
  (∀ᶠ (x : α) in la, p x) → ∀ (lb : Filter β), ∀ᶠ (x : α × β) in la ×ˢ lb, p x.1
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.ListSlice.toList_eq.match_1.eq_1 : ∀ (motive : Option ℕ → Sort u_1) (stop : ℕ) (h_1 : (stop : ℕ) → motive (some stop)) (h_2 : Unit → motive none),
  (match some stop with
    | some stop => h_1 stop
    | none => h_2 ()) =
    h_1 stop
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.rightCancelMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : One M₁] [inst_2 : Pow M₁ ℕ] [inst_3 : RightCancelMonoid M₂]
  (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y)
  (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n),
  Function.Injective.rightCancelMonoid f hf one mul npow =
    { toMonoid := Function.Injective.monoid f hf one mul npow, toIsRightCancelMul := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.WalkingParallelPair.one.sizeOf_spec : sizeOf CategoryTheory.Limits.WalkingParallelPair.one = 1
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.map_id : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α), M.map id = M
-- Mathlib.Computability.Reduce
OneOneReducible.disjoin_left : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : α → Prop} {q : β → Prop},
  p ≤₁ Sum.elim p q
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integral_Ioi_inv_one_add_sq : ∀ {i : ℝ}, ∫ (x : ℝ) in Set.Ioi i, (1 + x ^ 2)⁻¹ = Real.pi / 2 - Real.arctan i
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.edist_le_ediam : ∀ {α : Type u_1} {G : SimpleGraph α} {u v : α}, G.edist u v ≤ G.ediam
-- Init.Data.Option.Basic
/-- Equality with `none` is decidable even if the wrapped type does not have decidable equality.
 -/
Option.decidableEqNone : {α : Type u_1} → (o : Option α) → Decidable (o = none)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
/-- The multiplication operation for tensor products of externally `ι`-graded algebras.  -/
TensorProduct.gradedMul : (R : Type u_5) →
  {ι : Type u_6} →
    [inst : CommSemiring ι] →
      [Module ι (Additive ℤˣ)] →
        [DecidableEq ι] →
          (𝒜 : ι → Type u_7) →
            (ℬ : ι → Type u_8) →
              [inst_3 : CommRing R] →
                [inst_4 : (i : ι) → AddCommGroup (𝒜 i)] →
                  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] →
                    [inst_6 : (i : ι) → Module R (𝒜 i)] →
                      [inst_7 : (i : ι) → Module R (ℬ i)] →
                        [inst_8 : DirectSum.GRing 𝒜] →
                          [inst_9 : DirectSum.GRing ℬ] →
                            [DirectSum.GAlgebra R 𝒜] →
                              [DirectSum.GAlgebra R ℬ] →
                                TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ℬ) →ₗ[R]
                                  TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ℬ) →ₗ[R]
                                    TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ℬ)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_bot_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U : Submodule 𝕜 E}, U ⟂ ⊥
-- Init.Data.SInt.Lemmas
Int32.neg_mul_not_eq_add_mul : ∀ {a b : Int32}, -(a * ~~~b) = a + a * b
-- Mathlib.NumberTheory.FLT.Three
/-- Given `(S : Solution)`, we have that `λ ∣ (S.a + η * S.b)`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_mul_b : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ),
  hζ.toInteger - 1 ∣
    FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
      ↑⋯.unit * FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S)
-- Mathlib.Topology.Order.IsLUB
isLUB_of_mem_closure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {s : Set α} {a : α},
  a ∈ upperBounds s → a ∈ closure s → IsLUB s a
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instIntCast : {α : Type u_5} → [inst : NonUnitalNonAssocRing α] → IntCast (CentroidHom α)
-- Mathlib.Data.ENat.Basic
ENat.forall_ne_top : ∀ {p : ℕ∞ → Prop}, (∀ (x : ℕ∞), x ≠ ⊤ → p x) ↔ ∀ (x : ℕ), p ↑x
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` preserves colimits of shape `Jᵒᵖ`, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits of
shape `J`.  -/
CategoryTheory.Limits.preservesLimitsOfShape_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.PreservesLimitsOfShape J F.op
-- Init.RCases
/-- `⟨pat, ...⟩` is a pattern which matches on a tuple-like constructor
or multi-argument inductive constructor
 -/
Lean.Parser.Tactic.rcasesPat.tuple : Lean.ParserDescr
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
toDegLex_ofDegLex : ∀ {α : Type u_1} (a : DegLex α), toDegLex (ofDegLex a) = a
-- Init.Data.UInt.Bitwise
UInt32.xor_eq_zero_iff : ∀ {a b : UInt32}, a ^^^ b = 0 ↔ a = b
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- An affine subspace constructed from a point and a direction is nonempty.  -/
AffineSubspace.mk'_nonempty : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p : P) (direction : Submodule k V), (↑(AffineSubspace.mk' p direction)).Nonempty
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.instIsTopologicalGroup : ∀ {A : Type u_2} {E : Type u_6} [inst : Monoid A] [inst_1 : CommGroup E] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalGroup E], IsTopologicalGroup (A →ₜ* E)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.minSigmaOfOrd : {α : Type u} → {β : α → Type v} → [Ord α] → Min ((a : α) × β a)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.induction : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {motive : MonoidAlgebra R M → Prop} (x : MonoidAlgebra R M),
  motive 0 →
    (∀ (m : M) (r : R) (x : MonoidAlgebra R M),
        m ∉ x.coeff.support → r ≠ 0 → motive x → motive (MonoidAlgebra.single m r + x)) →
      motive x
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instSMul : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] →
          {M : Type u_3} →
            [inst_3 : Zero R] →
              [inst_4 : SMulZeroClass M R] → [ContinuousConstSMul M R] → SMul M (ContinuousMapZero X R)
-- Mathlib.Order.Filter.Prod
Filter.Eventually.curry : ∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {p : α × β → Prop},
  (∀ᶠ (x : α × β) in la ×ˢ lb, p x) → ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- **Alias** of the reverse direction of `OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq`. -/
OpenPartialHomeomorph.IsImage.of_symm_preimage_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t → e.IsImage s t
-- Mathlib.GroupTheory.OrderOfElement
Commute.orderOf_dvd_lcm_mul : ∀ {G : Type u_1} [inst : Monoid G] {x y : G}, Commute x y → orderOf y ∣ (orderOf x).lcm (orderOf (x * y))
-- Mathlib.Order.CompactlyGenerated.Basic
iSupIndep_iff_supIndep : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {ι : Type u_3} {f : ι → α},
  iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f
-- Mathlib.Topology.Order.Rolle
/-- A continuous function on a unordered closed interval with `f a = f b`
has a local extremum at some point of the corresponding unordered open interval.  -/
exists_isLocalExtr_uIoo : ∀ {X : Type u_1} {Y : Type u_2} [inst : ConditionallyCompleteLinearOrder X] [DenselyOrdered X]
  [inst_2 : TopologicalSpace X] [OrderTopology X] [inst_4 : LinearOrder Y] [inst_5 : TopologicalSpace Y]
  [OrderTopology Y] {f : X → Y} {a b : X},
  a ≠ b → ContinuousOn f (Set.uIcc a b) → f a = f b → ∃ c ∈ Set.uIoo a b, IsLocalExtr f c
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
integral_mulExpNegMulSq_comp_eq : ∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E}
  [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} {P' : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P']
  {A : Subalgebra ℝ (BoundedContinuousFunction E ℝ)},
  0 < ε →
    (∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') →
      ∀ {g : BoundedContinuousFunction E ℝ},
        g ∈ A → ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P = ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'
-- Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
AlgebraicGeometry.Polynomial.imageOfDf.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R),
  AlgebraicGeometry.Polynomial.imageOfDf f = {p | ∃ i, f.coeff i ∉ p.asIdeal}
-- Mathlib.Topology.Defs.Basic
TopologicalSpace.mk : {X : Type u} →
  (IsOpen : Set X → Prop) →
    IsOpen Set.univ →
      (∀ (s t : Set X), IsOpen s → IsOpen t → IsOpen (s ∩ t)) →
        (∀ (s : Set (Set X)), (∀ t ∈ s, IsOpen t) → IsOpen (⋃₀ s)) → TopologicalSpace X
-- Batteries.Data.String.Lemmas
String.back_eq_get_prev_rawEndPos : ∀ {s : String}, String.Legacy.back s = String.Pos.Raw.get s (String.Pos.Raw.prev s s.rawEndPos)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeffAddEquiv_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (self : SkewMonoidAlgebra k G),
  SkewMonoidAlgebra.coeffAddEquiv self = self.coeff
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
/-- Given an extension `α : H ⟶ L ⋙ H'`, this is the canonical extension
`K ⊠ H ⟶ (𝟭 E).prod L ⋙ K ⊠ H'` it induces through bifunctoriality of the external product.  -/
CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitRight : {V : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {D : Type u₂} →
        {D' : Type u₃} →
          {E : Type u₄} →
            [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} D'] →
                [inst_4 : CategoryTheory.Category.{v₄, u₄} E] →
                  {H : CategoryTheory.Functor D V} →
                    {L : CategoryTheory.Functor D D'} →
                      (H' : CategoryTheory.Functor D' V) →
                        (H ⟶ L.comp H') →
                          (K : CategoryTheory.Functor E V) →
                            CategoryTheory.MonoidalCategory.externalProduct K H ⟶
                              ((CategoryTheory.Functor.id E).prod L).comp
                                (CategoryTheory.MonoidalCategory.externalProduct K H')
-- Mathlib.CategoryTheory.Presentable.Type
CategoryTheory.Types.instIsCardinalLocallyPresentableType : ∀ (κ : Cardinal.{u}) [inst : Fact κ.IsRegular], CategoryTheory.IsCardinalLocallyPresentable (Type u) κ
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.comp.injEq : ∀ (a : Turing.ToPartrec.Code) (a_1 : Turing.PartrecToTM2.Cont') (a_2 : Turing.ToPartrec.Code)
  (a_3 : Turing.PartrecToTM2.Cont'),
  (Turing.PartrecToTM2.Cont'.comp a a_1 = Turing.PartrecToTM2.Cont'.comp a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.hygieneInfoNoAntiquot.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Rel
SetRel.inv_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) (S : SetRel β γ), (R.comp S).inv = S.inv.comp R.inv
-- Mathlib.Topology.Algebra.Group.Basic
IsOpen.leftCoset : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {U : Set G},
  IsOpen U → ∀ (x : G), IsOpen (x • U)
-- Mathlib.Order.SuccPred.LinearLocallyFinite
LinearLocallyFiniteOrder.instIsSuccArchimedeanOfLocallyFiniteOrder : ∀ {ι : Type u_1} [inst : LinearOrder ι] [LocallyFiniteOrder ι] [inst_2 : SuccOrder ι], IsSuccArchimedean ι
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.charpoly_of_card_eq_two : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  [Nontrivial R],
  Fintype.card n = 2 → M.charpoly = Polynomial.X ^ 2 - Polynomial.C M.trace * Polynomial.X + Polynomial.C M.det
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.periodicOrbit_length : ∀ {α : Type u_1} {f : α → α} {x : α}, (Function.periodicOrbit f x).length = Function.minimalPeriod f x
-- Mathlib.Topology.Order
instIndiscreteTopologyPUnit : IndiscreteTopology PUnit.{u_1 + 1}
-- Lean.Meta.Tactic.Grind.Util
Lean.Meta.Grind.reducePreMatchCond : Lean.Meta.Simp.DSimproc
-- Init.Data.Random
/-- The 'split' operation allows one to obtain two distinct random number
generators. This is very useful in functional programs (for example, when
passing a random number generator down to recursive calls).  -/
RandomGen.split : {g : Type u} → [self : RandomGen g] → g → g × g
-- Mathlib.Algebra.Module.Injective
/-- If we view `M` as a submodule of `N` via the injective linear map `i : M ↪ N`, then a submodule
between `M` and `N` is a submodule `N'` of `N`. To prove Baer's criterion, we need to consider
pairs of `(N', f')` such that `M ≤ N' ≤ N` and `f'` extends `f`.  -/
Module.Baer.ExtensionOf : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] → [inst_6 : Module R N] → (M →ₗ[R] N) → (M →ₗ[R] Q) → Type (max u_2 v)
-- Mathlib.Topology.Homeomorph.Defs
/-- Open quotient maps are preserved by postcomposing with a homeomorphism.  -/
Homeomorph.comp_isOpenQuotientMap_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : Y ≃ₜ Z) {f : X → Y}, IsOpenQuotientMap (⇑e ∘ f) ↔ IsOpenQuotientMap f
-- Mathlib.NumberTheory.Pell
/-- If `d` is a positive integer that is not a square, then there exists a solution
to the Pell equation `x^2 - d*y^2 = 1` with `x > 1` and `y > 0`.  -/
Pell.Solution₁.exists_pos_of_not_isSquare : ∀ {d : ℤ}, 0 < d → ¬IsSquare d → ∃ a, 1 < a.x ∧ 0 < a.y
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- The centroid lies in the affine span if the number of points,
converted to `k`, is not zero.  -/
centroid_mem_affineSpan_of_cast_card_ne_zero : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {s : Finset ι} (p : ι → P),
  ↑s.card ≠ 0 → Finset.centroid k s p ∈ affineSpan k (Set.range p)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
IsCovariantDerivativeOn.torsion_apply_eq_extend : ∀ {𝕜 : 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] [inst_6 : IsManifold I 2 M] [inst_7 : CompleteSpace E]
  {cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x} [inst_8 : CompleteSpace 𝕜]
  [inst_9 : FiniteDimensional 𝕜 E] (hcov : IsCovariantDerivativeOn E cov) {x : M} (X₀ Y₀ : TangentSpace I x),
  ((hcov.torsion x) X₀) Y₀ =
    (cov (FiberBundle.extend E Y₀) x) X₀ - (cov (FiberBundle.extend E X₀) x) Y₀ -
      VectorField.mlieBracket I (FiberBundle.extend E X₀) (FiberBundle.extend E Y₀) x
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_sup : ∀ {C : Type u_2} [inst : CommGroup C] {s t : Subgroup C} {x : C}, x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.eq_zero_of_eq_zero : ∀ {R : Type u} [inst : Semiring R], 0 = 1 → ∀ (p : Polynomial R), p = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the forward direction of the isomorphism
`PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂` w.r.t. the canonical maps to the colimit.  -/
CategoryTheory.Limits.PreservesColimit₂.ι_comp_isoColimitUncurryWhiskeringLeft₂_hom_assoc : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] (K₁ : CategoryTheory.Functor J₁ C₁)
  (K₂ : CategoryTheory.Functor J₂ C₂) (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G] [inst_6 : CategoryTheory.Limits.HasColimit K₁]
  [inst_7 : CategoryTheory.Limits.HasColimit K₂] (j : J₁ × J₂) {Z : C}
  (h : (G.obj (CategoryTheory.Limits.colimit K₁)).obj (CategoryTheory.Limits.colimit K₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι
        (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ K₁ K₂ G).hom h) =
    CategoryTheory.CategoryStruct.comp ((G.map (CategoryTheory.Limits.colimit.ι K₁ j.1)).app (K₂.obj j.2))
      (CategoryTheory.CategoryStruct.comp
        ((G.obj (CategoryTheory.Limits.colimit K₁)).map (CategoryTheory.Limits.colimit.ι K₂ j.2)) h)
-- Mathlib.Order.Atoms
isCoatomic_of_isAtomic_of_complementedLattice_of_isModular : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α] [ComplementedLattice α] [IsAtomic α],
  IsCoatomic α
-- Init.Data.Vector.Basic
/-- Delete the first element of a vector. Returns the empty vector if the input vector is empty.

We immediately simplify this to the `extract` operation, so there is no verification API for this function.
 -/
Vector.tail : {α : Type u_1} → {n : ℕ} → Vector α n → Vector α (n - 1)
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_empty_left : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] (t : Finset α), ∅.addEnergy t = 0
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.unitOfArray_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {a : Array α},
  Std.DHashMap.Raw.Const.unitOfArray a =
    ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity a)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.rightUnitor_inv_right_app : ∀ {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') (X : C),
  φ.rightUnitor.inv.right.app X = CategoryTheory.CategoryStruct.id (φ.right.obj X)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} {N₁ N₂ : M.Submodule}, N₁ = N₂ ↔ ∀ (X : Cᵒᵖ), N₁.obj X = N₂.obj X
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.instDivisionSemiring : {α : Type u} → {β : Type v} → {φ : Ultrafilter α} → [DivisionSemiring β] → DivisionSemiring ((↑φ).Germ β)
-- Init.Data.Array.Lemmas
Array.foldr_flip_append_eq_append : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {ys : Array β},
  Array.foldr (fun x acc => acc ++ f x) ys xs = ys ++ (Array.map f xs).reverse.flatten
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_inj : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : Zero α] [inst_1 : DecidableEq o]
  {M N : (i : o) → Matrix (m' i) (n' i) α}, Matrix.blockDiagonal' M = Matrix.blockDiagonal' N ↔ M = N
-- Lean.Data.Lsp.Basic
/-- The range of the text document to be manipulated.
To insert text into a document create a range where `start = end`.  -/
Lean.Lsp.TextEdit.range : Lean.Lsp.TextEdit → Lean.Lsp.Range