mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- `reverse` is involutive  -/
Quiver.HasInvolutiveReverse.inv' : ∀ {V : Type u_2} {inst : Quiver V} [self : Quiver.HasInvolutiveReverse V] {a b : V} (f : a ⟶ b),
  Quiver.reverse (Quiver.reverse f) = f
-- Mathlib.Order.OrderIsoNat
not_strictMono_of_wellFoundedGT : ∀ {α : Type u_1} [inst : Preorder α] [WellFoundedGT α] (f : ℕ → α), ¬StrictMono f
-- Mathlib.Algebra.GroupWithZero.Semiconj
SemiconjBy.inv_right_iff₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a x y : G₀}, SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- The 2-morphisms underlying the lax naturality constraint.  -/
CategoryTheory.Oplax.LaxTrans.naturality : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          (self : CategoryTheory.Oplax.LaxTrans F G) →
            {a b : B} →
              (f : a ⟶ b) →
                CategoryTheory.CategoryStruct.comp (self.app a) (G.map f) ⟶
                  CategoryTheory.CategoryStruct.comp (F.map f) (self.app b)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
/-- Auxiliary definition for `cechIsoCechNerve`.  -/
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      (U : CategoryTheory.Limits.FormalCoproduct C) →
        {T : C} →
          (hT : CategoryTheory.Limits.IsTerminal T) →
            (n : SimplexCategoryᵒᵖ) →
              U.cech.obj n ≅
                (CategoryTheory.Arrow.mk
                        ((CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)).cechNerve.obj
                  n
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsColoop.notMem_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {e : α} {C : Set α}, M.IsColoop e → M.IsCircuit C → e ∉ C
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.descFOne_zero_comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Z ⟶ Y)
  (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z),
  CategoryTheory.CategoryStruct.comp (J.cocomplex.d 0 1) (CategoryTheory.InjectiveResolution.descFOne f I J) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.descFZero f I J) (I.cocomplex.d 0 1)
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instPreservesLimitsOfShapeFunctorIndLimOfFinCategoryOfHasLimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w} [inst_1 : CategoryTheory.SmallCategory α]
  [CategoryTheory.FinCategory α] [CategoryTheory.Limits.HasLimitsOfShape α C] {I : Type v}
  [inst_4 : CategoryTheory.SmallCategory I] [inst_5 : CategoryTheory.IsFiltered I],
  CategoryTheory.Limits.PreservesLimitsOfShape α (CategoryTheory.Ind.lim I)
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.AsSmall.equiv_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.AsSmall.equiv.inverse = CategoryTheory.AsSmall.down
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.coe_inf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (p p' : L.Substructure M), ↑(p ⊓ p') = ↑p ∩ ↑p'
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.inv_mem_nonunits_iff : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) {x : K}, x⁻¹ ∈ A.nonunits ↔ x = 0 ∨ x ∉ A
-- Init.Data.Int.OfNat
Int.Nonneg.num_cert : ℤ → Bool
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₂ < a₁ → b₁ ≤ b₂ → Set.Icc a₁ b₁ ⊆ Set.Ioc a₂ b₂
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instDecidableEqFanin.decEq : (x x_1 : Std.Sat.AIG.Fanin) → Decidable (x = x_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanExt_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
  (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.spanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingSpan.left = iY
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Continuous.cpow : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f g : α → ℂ},
  Continuous f → Continuous g → (∀ (a : α), f a ∈ Complex.slitPlane) → Continuous fun x => f x ^ g x
-- Mathlib.Algebra.DirectSum.Ring
/-- The canonical map from ℕ to the zeroth component of a graded semiring.  -/
DirectSum.GSemiring.natCast : {ι : Type u_1} →
  {A : ι → Type u_2} →
    {inst : AddMonoid ι} → {inst_1 : (i : ι) → AddCommMonoid (A i)} → [self : DirectSum.GSemiring A] → ℕ → A 0
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coord_apply_ne : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) {i j : ι}, i ≠ j → (b.coord i) (b j) = 0
-- Mathlib.GroupTheory.Nilpotent
/-- The upper central series of a group is an ascending central series.  -/
Subgroup.upperCentralSeries_isAscendingCentralSeries : ∀ (G : Type u_1) [inst : Group G], Subgroup.IsAscendingCentralSeries (Subgroup.upperCentralSeries G)
-- Init.Data.Vector.Monadic
Vector.forIn'_pure_yield_eq_foldl : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  (f : (a : α) → a ∈ xs → β → β) (init : β),
  (forIn' xs init fun a m_1 b => pure (ForInStep.yield (f a m_1 b))) =
    pure
      (Vector.foldl
        (fun b x =>
          match x with
          | ⟨a, h⟩ => f a h b)
        init xs.attach)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
/-- The power series expansion of `Complex.sinh`.  -/
Complex.hasSum_sinh : ∀ (z : ℂ), HasSum (fun n => z ^ (2 * n + 1) / ↑(2 * n + 1).factorial) (Complex.sinh z)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.trans_tendsto : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {f'' : α → E''} {g'' : α → F''} {l : Filter α},
  f'' =O[l] g'' → Filter.Tendsto g'' l (nhds 0) → Filter.Tendsto f'' l (nhds 0)
-- Mathlib.Algebra.Group.Int.Defs
Int.instCommMonoid : CommMonoid ℤ
-- Mathlib.Data.Finset.Sups
Finset.card_diffs_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] (s t : Finset α),
  (s.diffs t).card ≤ s.card * t.card
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.aeval_U : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : Algebra R R'] (x : R') (n : ℤ),
  (Polynomial.aeval x) (Polynomial.Chebyshev.U R n) = Polynomial.eval x (Polynomial.Chebyshev.U R' n)
-- Mathlib.Data.Set.Image
Set.compl_compl_image : ∀ {α : Type u_1} [inst : BooleanAlgebra α] (s : Set α), compl '' compl '' s = s
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.isCyclicallyReduced_cons_append_iff : ∀ {α : Type u} {L : List (α × Bool)} {a b : α × Bool},
  FreeGroup.IsCyclicallyReduced (b :: L ++ [a]) ↔ FreeGroup.IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)
-- Mathlib.Logic.Function.Conjugate
/-- If `f` commutes with `g` and `g'`, then it commutes with `g ∘ g'`.  -/
Function.Commute.comp_right : ∀ {α : Type u_1} {f g g' : α → α}, Function.Commute f g → Function.Commute f g' → Function.Commute f (g ∘ g')
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Relation that needs to be well-formed in order for a loop over an iterator to terminate.
It is assumed that the `plausible_forInStep` predicate relates the input and output of the
stepper function.
 -/
Std.IteratorLoop.rel : (α : Type w) →
  (m : Type w → Type w') →
    {β : Type w} →
      [Std.Iterator α m β] → {γ : Type x} → (β → γ → ForInStep γ → Prop) → Std.IterM m β × γ → Std.IterM m β × γ → Prop
-- Mathlib.Data.ULift
ULift.ext_iff : ∀ {α : Type u} {x y : ULift.{u_1, u} α}, x = y ↔ x.down = y.down
-- Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
/-- To show that
```
P ---> X
|      |
v      v
Y ---> Z
```
is a pullback square, it suffices to check that
```
P ×[X] Uᵢ ---> Uᵢ
   |           |
   v           v
   Y --------> Z
```
is a pullback square for all `Uᵢ` in a cover of `X` for some subcanonical topology.
 -/
CategoryTheory.Precoverage.ZeroHypercover.isPullback_of_forall_isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C}
  [J.toGrothendieck.Subcanonical] [inst_2 : CategoryTheory.Limits.HasPullbacks C] [J.IsStableUnderBaseChange]
  {P X Y Z : C} (fst : P ⟶ X) (snd : P ⟶ Y) (f : X ⟶ Z) (g : Y ⟶ Z) (𝒰 : J.ZeroHypercover X),
  (∀ (i : 𝒰.I₀),
      CategoryTheory.IsPullback (CategoryTheory.Limits.pullback.snd fst (𝒰.f i))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst fst (𝒰.f i)) snd)
        (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) →
    CategoryTheory.IsPullback fst snd f g
-- Mathlib.Algebra.Lie.OfAssociative
LieSubalgebra.toEnd_eq : ∀ (R : Type u) (L : Type v) (M : Type w) [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]
  (K : LieSubalgebra R L) {x : ↥K}, (LieModule.toEnd R (↥K) M) x = (LieModule.toEnd R L M) ↑x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.modify.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β),
  m = m_1 → ∀ (a a_1 : α), a = a_1 → ∀ (f f_1 : β → β), f = f_1 → m.modify a f = m_1.modify a_1 f_1
-- Mathlib.CategoryTheory.Subobject.Comma
CategoryTheory.CostructuredArrow.projectQuotient.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} [inst_2 : CategoryTheory.Limits.HasFiniteColimits C]
  [inst_3 : CategoryTheory.Limits.PreservesFiniteColimits S] {A : CategoryTheory.CostructuredArrow S T}
  (a a_1 : CategoryTheory.Subobject (Opposite.op A)),
  a = a_1 → CategoryTheory.CostructuredArrow.projectQuotient a = CategoryTheory.CostructuredArrow.projectQuotient a_1
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coeFnAddMonoidHom_apply : ∀ {𝕜 : 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_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : AddMonoid G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffAdd I' n G] (a : ContMDiffMap I I' N G n) (a_1 : N), ContMDiffMap.coeFnAddMonoidHom a a_1 = a a_1
-- Mathlib.Analysis.Normed.Operator.Bilinear
Continuous.const_clm_comp : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  {σ₁₃ : 𝕜 →+* 𝕜₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃]
  [RingHomIsometric σ₁₂] {X : Type u_11} [inst_13 : TopologicalSpace X] {f : X → E →SL[σ₁₂] F},
  Continuous f → ∀ (g : F →SL[σ₂₃] G), Continuous fun x => g ∘SL f x
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.adjoin_le_centralizer_centralizer : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (s : Set A),
  StarAlgebra.adjoin R s ≤ StarSubalgebra.centralizer R ↑(StarSubalgebra.centralizer R s)
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `a`, `b`, and `c`, the derivative `f'` is nonnegative on
`Ioo a b` and nonpositive on `Ioo b c`. Then `f` attains its maximum on `Icc a c` at `b`.  -/
isMaxOn_Icc_of_deriv : ∀ {f : ℝ → ℝ} {a b c : ℝ},
  ContinuousAt f a →
    ContinuousAt f b →
      ContinuousAt f c →
        DifferentiableOn ℝ f (Set.Ioo a b) →
          DifferentiableOn ℝ f (Set.Ioo b c) →
            (∀ x ∈ Set.Ioo a b, 0 ≤ deriv f x) → (∀ x ∈ Set.Ioo b c, deriv f x ≤ 0) → IsMaxOn f (Set.Icc a c) b
-- Mathlib.LinearAlgebra.SymplecticGroup
/-- The matrix defining the canonical skew-symmetric bilinear form.  -/
Matrix.J : (l : Type u_1) → (R : Type u_2) → [DecidableEq l] → [CommRing R] → Matrix (l ⊕ l) (l ⊕ l) R
-- Init.Data.Array.Lemmas
Array.all_filter : ∀ {α : Type u_1} {xs : Array α} {p q : α → Bool}, (Array.filter p xs).all q = xs.all fun a => !p a || q a
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.exact₂_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ComposableArrows C 2) (hS : S.IsComplex),
  S.Exact ↔
    (S.sc' hS 0 1 2 CategoryTheory.ComposableArrows.exact₂_iff._proof_2
        CategoryTheory.ComposableArrows.exact₂_iff._proof_4
        CategoryTheory.ComposableArrows.isComplex₂_iff._proof_5).Exact
-- Mathlib.InformationTheory.Hamming
Hamming.instZero : {ι : Type u_2} → {β : ι → Type u_3} → [(i : ι) → Zero (β i)] → Zero (Hamming β)
-- Mathlib.RingTheory.DedekindDomain.PID
/-- If `p` is a prime in the Dedekind domain `R`, `S` an extension of `R` and `Sₚ` the localization
of `S` at `p`, then all primes in `Sₚ` are factors of the image of `p` in `Sₚ`.  -/
IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] (S : Type u_2) [inst_2 : CommRing S] [inst_3 : Algebra R S]
  [Module.IsTorsionFree R S] [Module.Finite R S] (p : Ideal R),
  p ≠ ⊥ →
    ∀ [inst_6 : p.IsPrime] {Sₚ : Type u_3} [inst_7 : CommRing Sₚ] [inst_8 : Algebra S Sₚ]
      [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [inst_10 : Algebra R Sₚ] [IsScalarTower R S Sₚ]
      [inst_12 : IsDedekindDomain Sₚ] [IsDomain S] {P : Ideal Sₚ},
      P.IsPrime → P ≠ ⊥ → P ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R Sₚ) p)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncKind.full.sizeOf_spec : sizeOf Lean.Lsp.TextDocumentSyncKind.full = 1
-- Qq.Macro
Qq.Impl.MVarSynth.level.inj : ∀ {unquotedMVar unquotedMVar_1 : Lean.LMVarId},
  Qq.Impl.MVarSynth.level unquotedMVar = Qq.Impl.MVarSynth.level unquotedMVar_1 → unquotedMVar = unquotedMVar_1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α}, a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.compLinearMap_inj : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (f : M₂ →ₗ[R] M),
  Function.Surjective ⇑f → ∀ (g₁ g₂ : M [⋀^ι]→ₗ[R] N), g₁.compLinearMap f = g₂.compLinearMap f ↔ g₁ = g₂
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- **Alias** of `WithSeminorms.continuous_of_isBounded`. -/
Seminorm.continuous_from_bounded : ∀ {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {F : Type u_7} {ι : Type u_9} {ι' : Type u_10} [inst : AddCommGroup E]
  [inst_1 : NormedField 𝕝] [inst_2 : Module 𝕝 E] [inst_3 : AddCommGroup F] [inst_4 : NormedField 𝕝₂]
  [inst_5 : Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [inst_6 : RingHomIsometric τ₁₂] {p : SeminormFamily 𝕝 E ι}
  {q : SeminormFamily 𝕝₂ F ι'} {x : TopologicalSpace E},
  WithSeminorms p →
    ∀ {x_1 : TopologicalSpace F}, WithSeminorms q → ∀ (f : E →ₛₗ[τ₁₂] F), Seminorm.IsBounded p q f → Continuous ⇑f
-- Lean.Server.GoTo
Lean.Server.GoToContext.mk.injEq : ∀ (doc : Lean.Server.DocumentMeta) (kind : Lean.Server.GoToKind) (infoTree? : Option Lean.Elab.InfoTree)
  (originInfo? : Option Lean.Elab.Info) (children : Lean.PersistentArray Lean.Elab.InfoTree)
  (doc_1 : Lean.Server.DocumentMeta) (kind_1 : Lean.Server.GoToKind) (infoTree?_1 : Option Lean.Elab.InfoTree)
  (originInfo?_1 : Option Lean.Elab.Info) (children_1 : Lean.PersistentArray Lean.Elab.InfoTree),
  ({ doc := doc, kind := kind, infoTree? := infoTree?, originInfo? := originInfo?, children := children } =
      { doc := doc_1, kind := kind_1, infoTree? := infoTree?_1, originInfo? := originInfo?_1,
        children := children_1 }) =
    (doc = doc_1 ∧ kind = kind_1 ∧ infoTree? = infoTree?_1 ∧ originInfo? = originInfo?_1 ∧ children = children_1)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusion : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (U : J.subschemeCover.I₀),
  CategoryTheory.CategoryStruct.comp (J.subschemeCover.f U) (AlgebraicGeometry.Scheme.IdealSheafData.inclusion h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom h U)
      (I.subschemeCover.f U)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.namespace.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.namespace = 1
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.sndCLM_apply : ∀ (R : Type u_3) (M : Type u_4) [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : CommSemiring R]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (x : TrivSqZeroExt R M), (TrivSqZeroExt.sndCLM R M) x = x.snd
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.triangle_assoc_comp_right_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).inv g)
      (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).hom =
    CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).inv
-- Mathlib.Order.UpperLower.Hom
LowerSet.iicsInfHom_apply : ∀ {α : Type u_1} [inst : CompleteLattice α] (a : α), LowerSet.iicsInfHom a = LowerSet.Iic a
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.path_image_Ico_of_ne : ∀ {x y : Circle}, x ≠ y → ⇑(x.path y) '' Set.Ico 0 1 = ⇑Circle.exp '' Set.Ico (↑x).arg (x.angleDiff y + (↑x).arg)
-- Init.Data.Array.Lemmas
Array.getElem_swapIfInBounds_right : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ} (hi : i < xs.size) (hj : j < (xs.swapIfInBounds i j).size),
  (xs.swapIfInBounds i j)[j] = xs[i]
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- One can reformulate being `Cⁿ` within a set at a point as continuity within this set at this
point, and being `Cⁿ` in the corresponding extended chart. This form states regularity of `f`
written in such a way that the set is restricted to lie within the domain/codomain of the
corresponding charts.
Even though this expression is more complicated than the one in `contMDiffWithinAt_iff`, it is
a smaller set, but their germs at `extChartAt I x x` are equal. It is sometimes useful to rewrite
using this in the goal.
 -/
contMDiffWithinAt_iff' : ∀ {𝕜 : 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'} {s : Set M} {x : M}
  {n : WithTop ℕ∞},
  ContMDiffWithinAt I I' n f s x ↔
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
        ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
        (↑(extChartAt I x) x)
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.ici_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (c : CategoryTheory.TransfiniteCompositionOfShape J f) (j : J), (c.ici j).F = ⋯.functor.comp c.F
-- Init.PropLemmas
forall_comm : ∀ {α : Sort u_2} {β : Sort u_1} {p : α → β → Prop}, (∀ (a : α) (b : β), p a b) ↔ ∀ (b : β) (a : α), p a b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
/-- The cotangent infinite sum representation.  -/
cot_series_rep : ∀ {x : ℂ},
  x ∈ Complex.integerComplement → ↑Real.pi * (↑Real.pi * x).cot = 1 / x + ∑' (n : ℕ+), (1 / (x - ↑↑n) + 1 / (x + ↑↑n))
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EquivalenceRelation.symmetry₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.EquivalenceRelation p₁ p₂), CategoryTheory.CategoryStruct.comp self.s p₁ = p₂
-- Mathlib.Control.Monad.Cont
LawfulMonadCont : (m : Type u → Type v) → [Monad m] → [MonadCont m] → Prop
-- Init.Data.Vector.Zip
Vector.zipWith_map_left : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {α' : Type u_3} {γ : Type u_4} {as : Vector α n} {bs : Vector β n} {f : α → α'}
  {g : α' → β → γ}, Vector.zipWith g (Vector.map f as) bs = Vector.zipWith (fun a b => g (f a) b) as bs
-- Mathlib.GroupTheory.NoncommPiCoprod
AddMonoidHom.noncommPiCoprod_single : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → AddMonoid (N i)] (ϕ : (i : ι) → N i →+ M)
  {hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)} [inst_3 : DecidableEq ι] (i : ι)
  (y : N i), (AddMonoidHom.noncommPiCoprod ϕ hcomm) (Pi.single i y) = (ϕ i) y
-- Mathlib.CategoryTheory.Retract
/-- Any object is a retract of itself.  -/
CategoryTheory.Retract.refl : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X : C) → CategoryTheory.Retract X X
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Pull back a `MulZeroClass` instance along an injective function.
See note [reducible non-instances].  -/
Function.Injective.mulZeroClass : {M₀ : Type u_1} →
  {M₀' : Type u_3} →
    [inst : MulZeroClass M₀] →
      [inst_1 : Mul M₀'] →
        [inst_2 : Zero M₀'] →
          (f : M₀' → M₀) → Function.Injective f → f 0 = 0 → (∀ (a b : M₀'), f (a * b) = f a * f b) → MulZeroClass M₀'
-- Mathlib.LinearAlgebra.Dual.Defs
MulOpposite.instModuleIsReflexive : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.IsReflexive R M], Module.IsReflexive R Mᵐᵒᵖ
-- Mathlib.Algebra.Group.Defs
/-- A mixin for right cancellative addition.  -/
IsRightCancelAdd : (G : Type u) → [Add G] → Prop