mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.comapIso_inv_subschemeι_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.comapIso f).inv (CategoryTheory.CategoryStruct.comp (I.comap f).subschemeι h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f I.subschemeι) h
-- Mathlib.Tactic.NormNum.GCD
/-- Given two integers, return their LCM and an equality proof.
Panics if `ex` or `ey` aren't integer literals.  -/
Mathlib.Meta.NormNum.proveIntLCM : (ex ey : Q(ℤ)) → (ed : Q(ℕ)) × Q(«$ex».lcm «$ey» = «$ed»)
-- Init.Data.List.TakeDrop
List.dropLast_eq_take : ∀ {α : Type u_1} {l : List α}, l.dropLast = List.take (l.length - 1) l
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_insertListIfNewUnit_of_contains_eq_false_of_mem : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k k' : α},
  (k == k') = true →
    ∀ {h : Std.Internal.List.containsKey k' (Std.Internal.List.insertListIfNewUnit l toInsert) = true},
      Std.Internal.List.containsKey k l = false →
        List.Pairwise (fun a b => (a == b) = false) toInsert →
          k ∈ toInsert → Std.Internal.List.getKey k' (Std.Internal.List.insertListIfNewUnit l toInsert) h = k
-- Mathlib.Data.Set.Function
Set.MapsTo.comp_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {s : Set β} {t : Set γ},
  Set.MapsTo g s t → ∀ (f : α → β), Set.MapsTo (g ∘ f) (f ⁻¹' s) t
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.HomologySequence.snakeInput_L₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j),
  (HomologicalComplex.HomologySequence.snakeInput hS i j hij).L₁ =
    (HomologicalComplex.opcyclesFunctor C c i).mapShortComplex.obj S
-- Init.Data.Array.Lemmas
Array.flatten_toArray_map : ∀ {α : Type u_1} {L : List (List α)}, (List.map List.toArray L).toArray.flatten = L.flatten.toArray
-- Mathlib.Algebra.Group.Action.Defs
vadd_iterate : ∀ {M : Type u_1} {α : Type u_5} [inst : AddMonoid M] [inst_1 : AddAction M α] (a : M) (n : ℕ),
  (fun x => a +ᵥ x)^[n] = fun x => n • a +ᵥ x
-- Mathlib.FieldTheory.Fixed
IsInvariantSubfield.mk : ∀ {M : Type u} [inst : Monoid M] {F : Type v} [inst_1 : Field F] [inst_2 : MulSemiringAction M F] {S : Subfield F},
  (∀ (m : M) {x : F}, x ∈ S → m • x ∈ S) → IsInvariantSubfield M S
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.lift_lift_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.MonObj B] (f g h : A ⟶ B),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
          CategoryTheory.MonObj.mul)
        h)
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g h)
          CategoryTheory.MonObj.mul))
      CategoryTheory.MonObj.mul
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.contains : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → Bool
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.coe_mulCoalgHom : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A],
  ⇑(Bialgebra.mulCoalgHom R A) = ⇑(LinearMap.mul' R A)
-- Mathlib.Topology.Sober
IsIrreducible.closure_genericPoint : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : QuasiSober α] {S : Set α} (hS : IsIrreducible S),
  IsClosed S → closure {hS.genericPoint} = S
-- Lean.Parser.Tactic
Lean.Parser.Tactic.matchAlts.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.LeftExactFunctor.of_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.PreservesFiniteLimits F],
  (CategoryTheory.LeftExactFunctor.of F).obj = F
-- Init.Data.Array.InsertIdx
Array.insertIdx_eraseIdx : ∀ {α : Type u} {a : α} {i j : ℕ} {as : Array α} (h₁ : i < as.size) (h₂ : j ≤ (as.eraseIdx i h₁).size),
  (as.eraseIdx i h₁).insertIdx j a h₂ =
    if h : i ≤ j then (as.insertIdx (j + 1) a ⋯).eraseIdx i ⋯ else (as.insertIdx j a ⋯).eraseIdx (i + 1) ⋯
-- Mathlib.Data.Matrix.Basic
/-- The `LinearEquiv` between spaces of matrices induced by a `LinearEquiv` between their
coefficients. This is `Matrix.map` as a `LinearEquiv`.  -/
LinearEquiv.mapMatrix : {m : Type u_2} →
  {n : Type u_3} →
    {R : Type u_7} →
      {S : Type u_8} →
        {α : Type u_11} →
          {β : Type u_12} →
            [inst : Semiring R] →
              [inst_1 : Semiring S] →
                [inst_2 : AddCommMonoid α] →
                  [inst_3 : AddCommMonoid β] →
                    [inst_4 : Module R α] →
                      [inst_5 : Module S β] →
                        {σᵣₛ : R →+* S} →
                          {σₛᵣ : S →+* R} →
                            [inst_6 : RingHomInvPair σᵣₛ σₛᵣ] →
                              [inst_7 : RingHomInvPair σₛᵣ σᵣₛ] → (α ≃ₛₗ[σᵣₛ] β) → Matrix m n α ≃ₛₗ[σᵣₛ] Matrix m n β
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.Algebra.instSMulCommClassCarrier : ∀ {S₀ : Type u₀} [inst : CommSemiring S₀] {S : Type u} [inst_1 : Semiring S] [inst_2 : Algebra S₀ S]
  {M : SemimoduleCat S}, SMulCommClass S S₀ ↑M
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.forgetToBoolAlg_full : (CategoryTheory.forget₂ FinBoolAlg BoolAlg).Full
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.comp_apply : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : AddCommMonoid E₃]
  [inst_6 : PartialOrder E₃] [inst_7 : Module R E₁] [inst_8 : Module R E₂] [inst_9 : Module R E₃] (g : E₂ →ₚ[R] E₃)
  (f : E₁ →ₚ[R] E₂) (x : E₁), (g.comp f) x = g.toLinearMap (f.toLinearMap x)
-- Mathlib.Order.Lex
toLex_ofLex : ∀ {α : Type u_1} (a : Lex α), toLex (ofLex a) = a
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
_private.Mathlib.RingTheory.PowerSeries.WeierstrassPreparation.0.PowerSeries.IsWeierstrassDivisorAt.seq.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match k.succ with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_2 k
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.ofStabilizer.addConjMap_apply : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a)
  (x : ↥(SubAddAction.ofStabilizer G a)), ↑((SubAddAction.ofStabilizer.conjMap hg) x) = g +ᵥ ↑x
-- Mathlib.Tactic.Linter.Whitespace
/-- The `whitespace` linter emits a warning if
* either a command does not start at the beginning of a line;
* or the "hypotheses segment" of a declaration does not coincide with its pretty-printed version.

In practice, this makes sure that the spacing in a typical declaration looks like
```lean
example (a : Nat) {R : Type} [Add R] : <not linted part>
```
as opposed to
```lean
example (a: Nat) {R:Type}  [Add  R] : <not linted part>
```
 -/
Mathlib.Linter.linter.style.whitespace : Lean.Option Bool
-- Init.Data.Rat.Lemmas
Rat.normalize_zero : ∀ {d : ℕ} (nz : d ≠ 0), Rat.normalize 0 d nz = 0
-- Mathlib.Algebra.Prime.Lemmas
DvdNotUnit.isUnit_of_irreducible_right : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p q : M}, DvdNotUnit p q → Irreducible q → IsUnit p
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the oriented angle between two vectors is `-π / 2`, the inner product of those vectors
(reversed) is zero.  -/
Orientation.inner_rev_eq_zero_of_oangle_eq_neg_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(-Real.pi / 2) → inner ℝ y x = 0
-- Mathlib.Order.Basic
Prod.instPreorder : {α : Type u_2} → {β : Type u_3} → [Preorder α] → [Preorder β] → Preorder (α × β)
-- Mathlib.Topology.WithTopology
WithTopology.instInfinite : ∀ {X : Type u_1} (t : TopologicalSpace X) [Infinite X], Infinite (WithTopology X t)
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `dist_triangle_left`.  -/
hammingDist_triangle_left : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] (x y z : (i : ι) → β i),
  hammingDist x y ≤ hammingDist z x + hammingDist z y
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.isBounded_image_toSnowflaking_iff : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : Bornology X] {s : Set X},
  Bornology.IsBounded (⇑Metric.Snowflaking.toSnowflaking '' s) ↔ Bornology.IsBounded s
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.add_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a b : X ⟶ Y), a + -b = a - b
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Submodule.reflection.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K K_1 : Submodule 𝕜 E) (e_K : K = K_1) [inst_3 : K.HasOrthogonalProjection], K.reflection = K_1.reflection
-- Lean.Elab.PreDefinition.WF.Fix
_private.Lean.Elab.PreDefinition.WF.Fix.0.Lean.Elab.WF.applyDefaultDecrTactic : Lean.MVarId → Lean.Elab.TermElabM Unit
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.toEquiv_injective : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞},
  Function.Injective Diffeomorph.toEquiv
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.χ_comp_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {𝒞₁ 𝒞₂ : CategoryTheory.Subobject.Classifier C} {X Y : C}
  (m : X ⟶ Y) [inst_1 : CategoryTheory.Mono m] {Z : C} (h : 𝒞₂.Ω ⟶ Z),
  CategoryTheory.CategoryStruct.comp (𝒞₁.χ m) (CategoryTheory.CategoryStruct.comp (𝒞₁.hom 𝒞₂) h) =
    CategoryTheory.CategoryStruct.comp (𝒞₂.χ m) h
-- Init.Data.List.Basic
/-- Returns the largest element of a non-empty list.

Examples:
* `[4].max (by decide) = 4`
* `[1, 4, 2, 10, 6].max (by decide) = 10`
 -/
List.max : {α : Type u} → [Max α] → (l : List α) → l ≠ [] → α
-- Mathlib.Topology.Sheaves.Skyscraper
/-- If `y ∉ closure {p₀}`, then the stalk of `skyscraperPresheaf p₀ A` at `y` is isomorphic to a
terminal object.
 -/
skyscraperPresheafStalkOfNotSpecializes : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          (A : C) →
            [inst_2 : CategoryTheory.Limits.HasTerminal C] →
              [inst_3 : CategoryTheory.Limits.HasColimits C] →
                {y : ↑X} → ¬p₀ ⤳ y → ((skyscraperPresheaf p₀ A).stalk y ≅ ⊤_ C)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesWithinOnBall.differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E} [CompleteSpace F],
  HasFPowerSeriesWithinOnBall f p s x r → DifferentiableOn 𝕜 f (insert x s ∩ Metric.eball x r)
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
/-- Independent Gaussian random variables are jointly Gaussian.  -/
ProbabilityTheory.iIndepFun.hasGaussianLaw : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Finite ι] {E : ι → Type u_3}
  [inst : (i : ι) → NormedAddCommGroup (E i)] [inst_1 : (i : ι) → MeasurableSpace (E i)]
  [∀ (i : ι), CompleteSpace (E i)] [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)]
  [inst_5 : (i : ι) → NormedSpace ℝ (E i)] {X : (i : ι) → Ω → E i},
  (∀ (i : ι), ProbabilityTheory.HasGaussianLaw (X i) P) →
    ProbabilityTheory.iIndepFun X P → ProbabilityTheory.HasGaussianLaw (fun ω x => X x ω) P
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerTMul_apply : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α]
  [inst_4 : Module R β] (A : Matrix l m α) (B : Matrix n p β) (i₁ : l) (i₂ : n) (j₁ : m) (j₂ : p),
  Matrix.kroneckerMap (TensorProduct.tmul R) A B (i₁, i₂) (j₁, j₂) = A i₁ j₁ ⊗ₜ[R] B i₂ j₂
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_eq_prime_iff : ∀ {G : Type u_1} [inst : AddMonoid G] [Nontrivial G] {p : ℕ},
  Nat.Prime p → (AddMonoid.exponent G = p ↔ ∀ (g : G), g ≠ 0 → addOrderOf g = p)
-- Init.Data.Vector.Attach
Vector.attach_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} {h : xs.size = n},
  (Vector.mk xs h).attach = Vector.mk (xs.attachWith (fun x => x ∈ Vector.mk xs h) ⋯) ⋯
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.id_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  (V : CategoryTheory.Endofunctor.Coalgebra F),
  (CategoryTheory.CategoryStruct.id V).f = CategoryTheory.CategoryStruct.id V.V
-- Mathlib.Data.ENNReal.Basic
ENNReal.toNNReal_eq_zero_iff : ∀ (x : ENNReal), x.toNNReal = 0 ↔ x = 0 ∨ x = ⊤
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Upgrading a functor `S ⥤ T` to a functor `S ⥤ Under X` and composing with the forgetful functor
`Under X ⥤ T` recovers the original functor.  -/
CategoryTheory.Functor.toUnderCompForget : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {S : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} S] →
        (F : CategoryTheory.Functor S T) →
          (X : T) →
            (f : (Y : S) → X ⟶ F.obj Y) →
              (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) →
                (F.toUnder X f ⋯).comp (CategoryTheory.Under.forget X) ≅ F
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.dartOfNeighborSet_toProd : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) (w : ↑(G.neighborSet v)), (G.dartOfNeighborSet v w).toProd = (v, ↑w)
-- Init.Data.BitVec.Basic
BitVec.getElem_eq_testBit_toNat : ∀ {w : ℕ} (x : BitVec w) (i : ℕ) (h : i < w), x[i] = x.toNat.testBit i
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.lift_of : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] {f : Polynomial R} [inst_1 : CommRing S] {i : R →+* S} {a : S}
  (h : Polynomial.eval₂ i a f = 0) {x : R}, (AdjoinRoot.lift i a h) ((AdjoinRoot.of f) x) = i x
-- Mathlib.RingTheory.Polynomial.UniqueFactorization
Polynomial.exists_irreducible_of_degree_pos : ∀ {R : Type u_1} [inst : CommSemiring R] [NoZeroDivisors R] [WfDvdMonoid R] {f : Polynomial R} [Nontrivial R],
  0 < f.degree → ∃ g, Irreducible g ∧ g ∣ f
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.opcyclesToCycles.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι)
  [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j],
  K.opcyclesToCycles i j = K.liftCycles (K.fromOpcycles i j) (c.next j) ⋯ ⋯
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : e.BoundaryGE i),
  (K.restrictionToTruncGE' e).f i =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi').hom
      (CategoryTheory.CategoryStruct.comp (K.pOpcycles i') (K.truncGE'XIsoOpcycles e hi' hi).inv)
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.forget₂_commMonCat_map_ofHom : ∀ {X Y : Type u} [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] (f : X →+ Y),
  (CategoryTheory.forget₂ AddCommGrpCat AddCommMonCat).map (AddCommGrpCat.ofHom f) = AddCommMonCat.ofHom f
-- Mathlib.Data.PNat.Basic
PNat.lt_add_right : ∀ (n m : ℕ+), n < n + m
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.of_isStableUnderColimitsOfShape.mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] {X Y : C} {f : X ⟶ Y}
  (hf : W.TransfiniteCompositionOfShape J f) [W.IsMultiplicative],
  (∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J],
      W.IsStableUnderColimitsOfShape J) →
    ∀ [W.RespectsIso], W f
-- Mathlib.NumberTheory.SumTwoSquares
/-- If `n` is a squarefree natural number, then `-1` is a square modulo `n` if and only if
`n` does not have a prime factor `q` such that `q % 4 = 3`.  -/
ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three : ∀ {n : ℕ}, Squarefree n → (IsSquare (-1) ↔ ∀ q ∈ n.primeFactors, q % 4 ≠ 3)
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- Choose a partial isomorphism witnessing that `X` and `Y` are birational over `S`.  -/
AlgebraicGeometry.Scheme.BirationalOver.partialIso : {S X Y : AlgebraicGeometry.Scheme} →
  (sX : X ⟶ S) → (sY : Y ⟶ S) → AlgebraicGeometry.Scheme.BirationalOver sX sY → X.PartialIso Y
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_Iio_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsCodirectedOrder α] {a : α} {f : β → ↑(Set.Iio a)} {l : Filter β},
  Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun x => ↑(f x)) l Filter.atBot
-- Mathlib.Data.Set.Function
Function.Surjective.surjOn : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β}, Function.Surjective f → Set.SurjOn f Set.univ t
-- Mathlib.Data.FunLike.IsApply
IsDivApply.div_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Div β}
  {inst_2 : Div F} [self : IsDivApply F α β] (f g : F) (x : α), (f / g) x = f x / g x
-- Mathlib.Algebra.Star.Pointwise
_private.Mathlib.Algebra.Star.Pointwise.0.Set.«term_⋆» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.exists_resolution_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y),
  ∃ g,
    CategoryTheory.CategoryStruct.comp g (HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj Y) =
      CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj X) f
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.coe_toEquiv_trans : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : AddCommMonoid C] [inst_4 : Module R A] [inst_5 : Module R B]
  [inst_6 : Module R C] [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C]
  {e₁₂ : A ≃ₗc[R] B} {e₂₃ : B ≃ₗc[R] C}, (↑e₁₂).trans ↑e₂₃ = ↑(e₁₂.trans e₂₃)
-- Mathlib.GroupTheory.Congruence.Defs
Con.toSetoid_injective : ∀ {M : Type u_1} [inst : Mul M], Function.Injective Con.toSetoid
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.toList.congr_simp : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxc.IsAlwaysFinite α] (r r_1 : Std.Rcc α),
  r = r_1 → r.toList = r_1.toList
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableCompletionItemKind : Hashable Lean.Lsp.CompletionItemKind
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRight_id_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y),
  f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom)
-- Lean.Parser.Level
Lean.Parser.Level.imax : Lean.Parser.Parser
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.eq_3 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.both with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_3 ()
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Hom.ext' : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} {f g : X ⟶ Y}, f.toHom = g.toHom → f = g
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.mem_powers_iff : ∀ {M : Type u_1} [inst : Monoid M] (x z : M), x ∈ Submonoid.powers z ↔ ∃ n, z ^ n = x
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
/-- The integral of `ω` along `[a -[ℝ] b]`, as a function of `b`, has derivative `ω a` at `b = a`.
This is a `HasFDerivAt` version assuming that `ω` is continuous on the whole space.  -/
HasFDerivAt.curveIntegral_segment_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F]
  [CompleteSpace F] {a : E} {ω : E → E →L[𝕜] F},
  Continuous ω → HasFDerivAt (fun x => ∫ᶜ (x : E) in Path.segment a x, ω x) (ω a) a
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instToJsonClientInfo.toJson : Lean.Lsp.ClientInfo → Lean.Json